Debian Science Logic packages

Agda est un langage de programmation fonctionnel typé de façon dépendante. Il possède des familles inductives, qui ressemblent aux GADT de Haskell, mais qui peuvent être indexées par des valeurs et pas seulement des types. Il possède également des modules de paramétrisations, des opérateurs mixfix, les caractères Unicode et une interface Emacs interactive (le vérificateur de type peut aider au développement du code).

Agda est également un assistant de preuve : C'est un système interactif pour écrire et vérifier des preuves. Agda est basé sur la théorie des types intuitifs, un système fondamental pour les mathématiques constructives développé par le logicien suédois Per Martin-Löf. Il possède de nombreux points communs avec d'autres assistants de preuves basés sur des types dépendants comme Coq, Epigram et NuPRL.

Ce méta-paquet fournit le mode emacs pour Agda, l'exécutable, la bibliothèque standard et la documentation.

Alt-Ergo est un démonstrateur de théorème automatique dédié à la vérification de programme. Il est basé sur CC(X), un algorithme de clôture de congruence paramétré par une théorie équationnelle X. Alt-Ergo possède des démonstrateurs intégrés pour la logique propositionnelle, l’arithmétique linéaire, les symboles de fonctions non interprétées, les symboles de fonctions associatives/commutatives, des tableaux polymorphes, les types d’enregistrements polymorphes personnalisés et des types d’énumération polymorphes. Il possède une gestion restreinte pour raisonner sur des types d’algèbre personnalisés, des quantifieurs de premier ordre et de l’arithmétique non linéaire.

Ce paquet fournit le démonstrateur avec une interface en ligne de commande.

Boolector est un solveur SMT (« satisfiability modulo theories ») efficace pour la théorie sans quantificateur de tableaux de bits combinée à l’extension de la théorie sans quantificateur de tableaux.

Clasp est un solveur d'ensembles de réponses pour des programmes logiques normaux (étendus). Il combine les capacités de modélisation de haut niveau de la programmation par ensembles de réponses (ASP) avec des techniques de pointe du domaine de la résolution de contraintes booléennes. L'algorithme claps principal se base sur l'apprentissage « nogood » basé sur les conflits qui s'est montré très efficace sur les problèmes de vérification de satisfiabilité (SAT). Contrairement à d'autres solveurs ASP avec apprentissage, clasp ne se base pas sur du logiciel hérité tel qu'un solveur SAT ou un autre solveur ASP existant. Au contraire, clasp a été développé directement pour la résolution d'ensembles de réponses basée sur l'apprentissage « nogood » mené par les conflits. Clasp peut être appliqué comme un solveur ASP (sur le format de sortie LPARSE), comme un solveur SAT (sur le format DIMACS/CNF simplifié) ou comme un solveur PB (sur le format OPB).

The coala tool translates an action language into a logic program under the answer set semantics. After being grounded by lparse or gringo, the logic program can be solved by an answer set solver such as clasp. At the moment coala is able to translate the action language AL, B, C, a subset of C+ and the action language CTAID. The type of input language can be specified with a command line option.

Cbc (Coin-or branch and cut) est un solveur de programmes en variables mixtes libre écrit en C++. Il peut être utilisé en tant que bibliothèque appelable ou comme un exécutable autonome.

Ce paquet fournit l'exécutable cbc.

SYMPHONY est un solveur libre et générique de programmes linéaires en nombres mixtes (MILP – «⋅Mixed-Integer Linear Programs⋅»), une bibliothèque et un cadriciel pour implémenter des solveurs personnalisés. SYMPHONY a un certain nombre de capacités évoluées, telles que la possibilité de résoudre des MILP multiobjectifs, la possibilité d'utiliser un démarrage à chaud de sa procédure de résolution et la capacité d'effectuer des analyses de sensibilité basiques.

SYMPHONY fait partie de l'initiative COIN-OR (« Computational Infrastructure for Operations Research »).

Ce paquet fournit l'exécutable symphony.

Coq est un assistant de preuve pour la logique d'ordre supérieur, qui permet le développement de programmes d'ordinateur correspondant à une spécification formelle. Il est développé en Objective Caml et Camlp5.

Ce paquet fournit coqtop, une interface en ligne de commande pour Coq.

Une interface graphique pour Coq est fournie dans le paquet coqide. On peut aussi utiliser Coq avec ProofGeneral, qui permet l'édition de preuves dans Emacs et XEmacs. Pour cela, le paquet proofgeneral doit être installé.

CVC3 is an automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination.

CVC3 is the last offspring of a series of popular SMT provers, which originated at Stanford University with the SVC system. In particular, it builds on the code base of CVC Lite, its most recent predecessor. Its high level design follows that of the Sammy prover.

CVC3 works with a version of first-order logic with polymorphic types and has a wide variety of features including:

• several built-in base theories: rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bit vectors, and equality over uninterpreted function symbols;
• support for quantifiers;
• an interactive text-based interface;
• rich C, C++, and Java APIs for embedding in other systems;
• proof and model generation abilities;
• predicate subtyping;
• essentially no limit on its use for research or commercial purposes (see license).

This package contains the CVC3 command line program.

CVC4 is an efficient automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination.

CVC4 is intended to be an open and extensible SMT engine, and it can be used as a stand-alone tool or as a library. It is the fourth in the Cooperating Validity Checker family of tools (also including CVC, CVC Lite and CVC3). CVC4 has been designed to increase the performance and reduce the memory overhead of its predecessors.

This package contains binaries needed to use CVC4 as a stand-alone tool.

DepQBF is a search-based solver for quantified boolean formulae (QBF) in prenex conjunctive normal form. It is based on the DPLL algorithm for QBF, called QDPLL, with conflict-driven clause and solution-driven cube learning. By analyzing the syntactic structure of a formula, DepQBF tries to identify independent variables. In general, information on independent variables can be represented in the formal framework of dependency schemes. DepQBF computes the so-called "standard dependency scheme" of a given formula. In addition to other benefits, information on independent variables often increases the freedom for decision making and clause learning.

La solution actuelle fixe les solveurs pour œuvrer sur des programmes avec des variables libres. Par conséquent, un « grounder » (ancrage situationnel) est nécessaire, qui, un programme d’entrée étant indiqué avec des variables de premier ordre, calcule le programme « ground » équivalent (variables libres).

Ce paquet fournit les outils suivants :

 – gringo : un grounder qui, un programme d’entrée étant indiqué avec des
   variables de premier ordre, calcule le programme « ground » équivalent
   (variables libres) au format aspif. Sa sortie peut être traitée plus
   tard avec clasp, un solveur « answer set » (programmation déclarative).
   À partir des séries cinq de gringo, la sortie de celui-ci n’est plus
   directement compatible avec les solveurs tels smodels ou cmodels lisant
   le format smodels. Lpconvert est à utiliser pour convertir le format
   aspif au format smodels ;
 – clingo : une combinaison de gringo et clasp dans un système
   monolithique. De cette façon, il propose plus de contrôle sur les
   traitements de grounding et de résolution que gringo et clasp peuvent
   proposer individuellement : la résolution à répétition ;
 – lpconvert : un convertisseur entre les formats aspif de gringo et
   smodels ;
 – reify : un petit utilitaire qui réifie les programmes logiques donnés
   au format aspif. Il produit un ensemble d’éléments pouvant être traités
   ultérieurement avec gringo.

HOL Light est un démonstrateur de théorème interactif pour la logique d’ordre supérieur avec un cœur logique très simple exécuté dans toplevel OCaml. HOL Light est célèbre pour la vérification de l’arithmétique en virgule flottante ainsi que pour le projet Flyspeck, qui se veut la formalisation de Tom Hales de sa preuve de la conjecture de Kepler.

Le système HOL est un assistant de preuve interactif dans une logique d'ordre supérieur. Il est particulièrement remarquable par son haut degré de programmabilité, grâce au méta-langage ML. HOL a de nombreux usages qui vont de la formalisation en mathématiques pures à la vérification de matériel industriel. HOL est utilisé par des institutions universitaires et des industries du monde entier.

Ce logiciel convertit une formule logique temporelle linéaire (ltl) en un automate de Büchi. L'automate résultant peut être utilisé, par exemple, pour vérifier un modèle où il représente une propriété du modèle à vérifier (par exemple un réseau de Petri).

MACE est un programme qui recherche les modèles finis du premier ordre et les formules propositionnelles, développé au Laboratoire National d'Argonne aux USA.

Ce paquet fournit ANDLP qui appelle directement la procédure de décision propositionnelle, au cœur de MACE.

MACE est un programme d'accompagnement complémentaire de OTTER qui recherche les réfutations de la même classe de prédicats. Plus particulièrement, avec une conjecture du premier ordre, OTTER recherchera une preuve et MACE recherchera un contre-exemple depuis le même fichier d'entrée.

Maria est un outil puissant conçu pour aider les ingénieurs à modéliser et résoudre des problèmes liés à la concurrence dans les systèmes de calcul parallèle et distribué.

Maria trouve les impasses et les violations de sécurité ou de besoins de « liveness » en explorant tous les états pouvant être atteints depuis l'état initial du système. L'outil gère des dizaines ou centaines de milliers d'états atteignables et d'actions activées.

La puissance d'expression du formalisme de Maria est proche des langages de programmation de haut niveau grâce à un système de type de données riche et à de puissantes opérations algébriques.

Matita is a graphical interactive theorem prover based on the Calculus of (Co)Inductive Constructions.

Maude est un langage et un système réflexif haute performance gérant à la fois la spécification et la programmation de la réécriture logique et équationnelle d'une large gamme d'applications. Maude a été influencé dans une large mesure par le langage OBJ3, qui peut être considéré comme un sous-langage de logique équationnelle. Outre la prise en charge de la spécification et la programmation équationnelle, Maude gère aussi la réécriture de calcul logique.

La réécriture logique suit une logique de changements concurrents qui peut traiter naturellement l'état et des calculs concurrents. Il comporte des propriétés intéressantes, en tant que cadriciel sémantique généraliste, pour donner des sémantiques d'exécutable à une large gamme de langages et de modèles de concurrence. En particulier, il gère très bien le calcul concurrent orienté objet. C'est parce qu'une réécriture logique donne un bon cadriciel sémantique que cela donne aussi un bon cadriciel logique, c'est-à-dire une métalogique où de nombreuses autres logiques peuvent être représentées et exécutées naturellement.

Maude gère de manière systématique et efficace la réflexion logique. Cela rend Maude notablement extensible et puissant, gérant une algèbre extensible d'opérations de création de module et permettant de faire beaucoup de métaprogrammation d’applications de métalangage avancées. En effet, parmi les applications les plus intéressantes de Maude, on trouve les applications en métalangage, où Maude est utilisé pour créer des environnements exécutables pour une variété de logiques, de démonstrateurs automatiques de théorèmes, de langages et de modèles de calcul.

Maude trouve tout son intérêt auprès de la communauté biomédicale pour modéliser et analyser des systèmes biologiques.

MinSat+ est un solveur pour l’optimisation pseudo booléenne (Pseudo-Boolean Optimization, c'est-à-dire l’optimisation linéaire en nombres entiers) basée sur SAT-solver de MiniSat. Il gère l’optimisation de fonction objectif linéaire, sujette à un ensemble de contraintes linéaires. Les variables de la fonction objectif sont booléennes, c'est-à-dire, doivent être zéro ou un. L’optimisation pseudo booléenne peut être utilisée pour résoudre plusieurs sortes de problèmes d’optimisation combinatoire. Cette version de Minisat+ est compilée avec la prise en charge de grands nombres pour les coefficients de contrainte.

MONA est un outil pour traduire des formules de logiques WS1S ou WS2S dans des automates avec un nombre fini d'état représentés par des diagrammes de décision binaire (BDD). Les formules peuvent exprimer des modèles de recherche, des propriétés temporelles de systèmes réactifs, des contraintes d’analyse d’arbre, etc. MONA analyse aussi l’automate résultant de la compilation et détermine si la formule est valable ou non, et si elle ne l’est pas, crée un contre-exemple.

La documentation est disponible sur le site web de MONA, http://www.brics.dk/mona/.

Malgré la complétude NP des problèmes de satisfaisabilité de formules booléennes (SAT), les solveurs SAT sont souvent capables de trancher dans un délai raisonnable. Comme tous les autres problèmes de complétude NP sont réductibles à SAT, les solveurs sont devenus des outils polyvalents pour cette classe de problèmes.

PicoSAT est un solveur SAT qui s’avère être plus rapide pour des cas industriels que MiniSAT 2.0, et qui peut générer des démonstrations et des « core » en mémoire.

« Proof General » est un mode majeur d'Emacs pour le transformer en système d’assistant de preuves interactif afin d'écrire des preuves mathématiques formelles en utilisant toute une variété de théorèmes.

Ce paquet fournit la prise en charge de Proof General pour Coq. (Il n’existe pas d’autres assistant de preuve pouvant être raisonnablement pris en charge.)

Ce paquet fournit le démonstrateur de théorème de résolution et « paramodulation » Prover9 et le générateur de contre-exemples Mace4.

Prover9 est un démonstrateur de théorème automatique de calcul des prédicats du premier ordre. C’est un successeur du démonstrateur Otter. Prover9 utilise les techniques d’inférence de résolution et paramodulation ordonnées avec sélection de littéraux.

Le programme Mace4 recherche des modèles finis satisfaisant des propositions d’équation du premier ordre, du même genre que celles que Prover9 accepte. Si la proposition est la négation d’une conjecture, tout modèle trouvé par Mace4 est un contre-exemple de cette conjecture.

Mace4 peut être un complément précieux à Prover9, recherchant des contre-exemples avant (ou simultanément) l’utilisation de Prover9 pour la recherche de preuve. Il peut aussi être utilisé pour aider à déboguer des propositions et formules d’entrée pour Prover9.

L'objectif de la bibliothèque SAT4J est de proposer des solveurs SAT efficaces en Java. Par rapport au projet OpenSAT, la bibliothèque SAT4J répond principalement aux besoins des utilisateurs de « boîtes noires » SAT qui veulent intégrer les technologies SAT dans leur application sans se soucier des détails. Le projet SAT4J tente aussi de fournir une base de travail pour les chercheurs.

SPASS est un démonstrateur automatique de théorème basé sur la saturation pour la logique du premier ordre égalitaire. Il est unique à cause de la combinaison de calcul de recouvrement (superposition calculus) avec des règles spécifiques d’inférence ou réduction pour des genres (types) et une règle de dissociation pour l’analyse de cas motivés par une règle bêta de tableaux analytiques et l’analyse de cas employé dans la procédure de Davis-Putnam. De plus, SPASS fournit une traduction sophistiquée de forme normale conjonctive (clause normal form).

Ce paquet consiste en un binaire SPASS/FLOTTER, la documentation et une petite collection d’exemples. La collection d’outils fournit le vérificateur de preuve pcs, les traducteurs de syntaxe dfg2otter et dfg2tptp, et le joli afficheur ASCII dfg2ascii.

Toulbar2 is an exact discrete optimization tool for Graphical Models such as Cost Function Networks, Markov Random Fields, Weighted Constraint Satisfaction Problems and Bayesian Nets.

Why est une interface de générateur de vérification de conditions (VCG : verification conditions generator) pour d'autres outils de vérification. Il utilise un langage puissant incluant des fonctions d'ordre supérieur, le polymorphisme, les références, les tableaux et les exceptions. Il construit des obligations de preuve pour plusieurs systèmes : les assistants de preuve Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar et les procédures de décision Simplify, Alt-Ergo, Yices, CVC Lite et haRVey.

Why3 est une plateforme pour la vérification déductive de programme. Elle fournit un langage riche pour la spécification et la programmation, appelé WhyML, et repose sur des démonstrateurs externes de théorème, à la fois automatiques et interactifs, pour remplir les conditions de vérification. Why3 est fournie avec une bibliothèque standard de théories logiques (arithmétique des nombres entiers et réels, opérations booléennes, ensembles et leurs relations, etc.) et des structures de données de programmation (tableaux, files d’attente, tables de hachage, etc.). Un utilisateur peut écrire directement des programmes WhyML et obtenir des programmes OCaml correct-par-construction à travers un mécanisme automatique d’extraction. WhyML est aussi utilisé comme langage intermédiaire pour la vérification de de programmes C, Java ou Ada.

Why3 est une réimplémentation complète de l’ancienne plateforme Why. Parmi les nouvelles caractéristiques, il y a de nombreuses extensions pour le langage utilisé, une nouvelle architecture pour appeler des démonstrateurs externes et une API bien conçue permettant d’utiliser Why3 comme bibliothèque logicielle. L’accent est porté sur la modularité et la généricité, permettant à l’utilisateur final de facilement réutiliser des formalisations Why3 ou d’ajouter la prise en charge de nouveaux démonstrateurs.

Issu de Microsoft Research, Z3 est un justificateur de théorème à la pointe de l’art. Il peut être utilisé pour vérifier l’adéquation de formules logiques par rapport à une ou plusieurs théories. Z3 permet une incontestable adéquation dans l’analyse de logiciels et d’outils de vérification, étant donné que quelques logiciels communs établissent des correspondances directement dans les théories prises en charge.

Le format d’entrée de Z3 est une extension du standard SMT-LIB 2.0.

L'optimiseur Coin-MP est un solveur libre faisant partie du projet COIN-OR qui est une initiative pour stimuler le développement de logiciels libres pour la communauté de recherche opérationnelle.

CoinMP est une bibliothèque API en C prenant en charge la plupart des fonctions des projets CLP (Coin LP), CBC (Coin Branch-and-Cut) et CGL (Cut Generation Library).

Ce paquet fournit les fichiers nécessaires pour construire des applications utilisant libCoinMP.