Debian Science Project
Summary
Logic
Debian Science Logic packages

This metapackage is part of the Debian Pure Blend "Debian Science" and installs packages related to Computational Logic. It contains formula transformation tools, solvers for formulas specified in various logics, interactive proof systems, etc.

Description

For a better overview of the project's availability as a Debian package, each head row has a color code according to this scheme:

If you discover a project which looks like a good candidate for Debian Science to you, or if you have prepared an unofficial Debian package, please do not hesitate to send a description of that project to the Debian Science mailing list

Links to other tasks

Debian Science Logic packages

Official Debian packages with high relevance

Agda
langage de programmation fonctionnel typé de façon dépendante
Versions of package agda
ReleaseVersionArchitectures
wheezy2.3.0.1-2all
jessie2.4.0.2-2all
sid2.6.0.1-1all
bullseye2.6.0.1-1all
buster2.5.4.1-3all
stretch2.5.1.1-3all
Debtags of package agda:
rolemetapackage
Popcon: 0 users (0 upd.)*
Versions and Archs
License: DFSG free
Git

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
démonstrateur automatique dédié à la vérification de programme
Versions of package alt-ergo
ReleaseVersionArchitectures
bullseye2.0.0-5amd64,arm64,armel,i386,mips64el,mipsel,ppc64el,s390x
stretch1.30-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
squeeze0.91-2amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy0.94-2amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie0.95.2-3amd64,armel,armhf,i386
sid2.0.0-5amd64,arm64,armel,i386,mips64el,mipsel,ppc64el,s390x
buster2.0.0-3amd64,arm64,armel,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package alt-ergo:
roleprogram
uitoolkitgtk
Popcon: 10 users (17 upd.)*
Versions and Archs
License: DFSG free
Git

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és, 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 des interfaces en ligne de commande et graphique.

Boolector
solveur SMT pour les vecteurs de bits et les tableaux
Maintainer: Michael Tautschnig
Versions of package boolector
ReleaseVersionArchitectures
wheezy1.4.ffc2089.100608-1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie1.5.118.6b56be4.121013-1amd64,armel,armhf,i386
sid1.5.118.6b56be4.121013-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster1.5.118.6b56be4.121013-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch1.5.118.6b56be4.121013-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye1.5.118.6b56be4.121013-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
squeeze1.4.ffc2089.100608-1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
Debtags of package boolector:
roleprogram
Popcon: 6 users (1 upd.)*
Versions and Archs
License: DFSG free

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
solveur d'ensemble de réponses par apprentissage nogood basé sur les conflits
Versions of package clasp
ReleaseVersionArchitectures
jessie3.1.0-1amd64,armel,armhf,i386
wheezy2.0.6-2amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
sid3.3.4-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bullseye3.3.4-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster3.3.4-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch3.2.1-3amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
upstream3.3.5
Debtags of package clasp:
roleprogram
Popcon: 66 users (45 upd.)*
Newer upstream!
License: DFSG free
Git

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).

Coala
translates action languages into answer set programs
Versions of package coala
ReleaseVersionArchitectures
jessie1.0.1-5amd64,armel,armhf,i386
wheezy1.0.1-5amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
Debtags of package coala:
roleprogram
Popcon: 0 users (0 upd.)*
Versions and Archs
License: DFSG free
Git

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.

Coinor-cbc
solveur de programmes en variables mixtes par branch-and-cut COIN-OR
Versions of package coinor-cbc
ReleaseVersionArchitectures
sid2.9.9+repack1-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster2.9.9+repack1-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch2.8.12-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie2.8.12-1amd64,armel,armhf,i386
bullseye2.9.9+repack1-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
upstream2.10.3
Popcon: 86 users (33 upd.)*
Newer upstream!
License: DFSG free
Git

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.

Coinor-symphony
solveur COIN-OR pour les programmes linéaires en nombres mixtes
Versions of package coinor-symphony
ReleaseVersionArchitectures
buster5.6.16+repack1-1.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie5.6.1-1amd64,armel,armhf,i386
stretch5.6.1-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye5.6.16+repack1-1.1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
sid5.6.16+repack1-1.1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
upstream5.6.17
Popcon: 18 users (4 upd.)*
Newer upstream!
License: DFSG free
Git

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
outil d'aide à la preuve pour la logique d'ordre supérieur (environnement interactif et compilateur)
Versions of package coq
ReleaseVersionArchitectures
sid8.9.1-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bullseye8.9.1-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
squeeze8.2.pl2+dfsg-1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy8.3.pl4+dfsg-2amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie8.4pl4dfsg-1amd64,armel,armhf,i386
buster8.9.0-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch8.6-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
upstream8.10.2
Debtags of package coq:
develcompiler
fieldmathematics
interfacecommandline, text-mode
roleprogram
scopeutility
uitoolkitncurses
Popcon: 48 users (53 upd.)*
Newer upstream!
License: DFSG free
Git

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.

Le paquet proofgeneral permet aux démonstrations d’être éditées en utilisant Emacs et XEmacs.

The package is enhanced by the following packages: libaac-tactics-ocaml libssreflect-ocaml
Cvc3
Automatic theorem prover for SMT problems
Maintainer: Morgan Deters (Adrian Bunk)
Versions of package cvc3
ReleaseVersionArchitectures
wheezy2.4.1-4amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie2.4.1-5amd64,armel,armhf,i386
stretch2.4.1-5.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
squeeze2.2-13amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
Debtags of package cvc3:
interfacecommandline
roleprogram
Popcon: 5 users (0 upd.)*
Versions and Archs
License: DFSG free

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.

The package is enhanced by the following packages: cvc3-el
Cvc4
automated theorem prover for SMT problems
Versions of package cvc4
ReleaseVersionArchitectures
buster1.6-2amd64,i386,mips,mips64el,mipsel
bullseye1.6-2amd64,i386,mips64el,mipsel
sid1.6-2amd64,i386,mips64el,mipsel
Popcon: 8 users (5 upd.)*
Versions and Archs
License: DFSG free
Git

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
solver for quantified boolean formulae
Versions of package depqbf
ReleaseVersionArchitectures
buster5.01-3amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye5.01-3amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
sid5.01-3amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
jessie3.04-1amd64,armel,armhf,i386
wheezy0.1-1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
stretch5.01-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
upstream6.03
Popcon: 6 users (2 upd.)*
Newer upstream!
License: DFSG free
Git

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.

Gringo
outils de « grounding » pour des programmes logiques (disjonctifs)
Versions of package gringo
ReleaseVersionArchitectures
wheezy3.0.4-3amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie4.4.0-1amd64,armel,armhf,i386
stretch5.1.0-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster5.3.0-10amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye5.3.0-10amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
sid5.3.0-10amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
upstream5.4.0
Debtags of package gringo:
roleprogram
Popcon: 75 users (43 upd.)*
Newer upstream!
License: DFSG free
Git

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.
Please cite: Martin Gebser, Roland Kaminski, Benjamin Kaufmann and Torsten Schaub: Multi-shot ASP solving with clingo. Theory and Practice of Logic Programming :1–56 (2018)
Hol-light
HOL Light theorem prover
Versions of package hol-light
ReleaseVersionArchitectures
sid20190729-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
wheezy20120602-1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie20131026-1amd64,armel,armhf,i386
stretch20170109-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Popcon: 2 users (0 upd.)*
Versions and Archs
License: DFSG free
Git

HOL Light is an interactive theorem prover for Higher-Order Logic with a very simple logical core running in an OCaml toplevel. HOL Light is famous for the verification of floating-point arithmetic as well as for the Flyspeck project, which aimed at the formalization of Tom Hales' proof of the Kepler conjecture.

Hol88
Higher Order Logic (logique d'ordre supérieur), image système
Maintainer: Camm Maguire
Versions of package hol88
ReleaseVersionArchitectures
buster2.02.19940316-35amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie2.02.19940316-28amd64,armel,armhf,i386
bullseye2.02.19940316-35amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
stretch2.02.19940316-33amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
squeeze2.02.19940316-13.1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy2.02.19940316-15amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
sid2.02.19940316-35amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
Debtags of package hol88:
uitoolkitncurses
Popcon: 5 users (3 upd.)*
Versions and Archs
License: DFSG free

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.

Lbt
Convertit des formules LTL en automates Büchi
Versions of package lbt
ReleaseVersionArchitectures
sid1.2.2-6amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
wheezy1.2.2-5amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
squeeze1.2.2-4amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
jessie1.2.2-5amd64,armel,armhf,i386
stretch1.2.2-6amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster1.2.2-6amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye1.2.2-6amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
Debtags of package lbt:
fieldmathematics
interfacecommandline
roleprogram
scopeutility
useconverting
Popcon: 6 users (5 upd.)*
Versions and Archs
License: DFSG free
Git

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).

Mace2
programme de recherche de modèles finis de prédicats du premier ordre
Versions of package mace2
ReleaseVersionArchitectures
jessie3.3f-1.1amd64,armel,armhf,i386
squeeze3.3f-1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy3.3f-1.1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
Debtags of package mace2:
roleprogram
usesearching
Popcon: 0 users (0 upd.)*
Versions and Archs
License: DFSG free

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
analyseur d'accessibilité pour les réseaux de systèmes algébriques
Versions of package maria
ReleaseVersionArchitectures
stretch1.3.5-4.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid1.3.5-4.1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
squeeze1.3.5-2amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy1.3.5-4amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
bullseye1.3.5-4.1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster1.3.5-4.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie1.3.5-4amd64,armel,armhf,i386
Debtags of package maria:
develtesting-qa
fieldmathematics
interfacetext-mode
roleprogram
scopeutility
uitoolkitncurses
Popcon: 7 users (6 upd.)*
Versions and Archs
License: DFSG free
Git

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
assistant de preuve interactif
Versions of package matita
ReleaseVersionArchitectures
stretch0.99.3-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
wheezy0.99.1-1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
squeeze0.5.8-2amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
sid0.99.3-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
jessie0.99.1-3amd64,armel,armhf,i386
Debtags of package matita:
fieldmathematics
interfacecommandline, x11
roleprogram
uitoolkitgtk
usechecking
x11application
Popcon: 10 users (0 upd.)*
Versions and Archs
License: DFSG free
Git

Matita est un assistant de preuve, graphique et interactif basé sur le calcul des constructions avec types de données inductives [CoC — Calculus of (Co)Inductive Constructions].

Screenshots of package matita
Maude
cadriciel logique de haute performance
Versions of package maude
ReleaseVersionArchitectures
jessie2.6-6amd64,armel,armhf,i386
wheezy2.6-2amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
bullseye2.7-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
sid2.7-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster2.7-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch2.7-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package maude:
uitoolkitncurses
Popcon: 5 users (3 upd.)*
Versions and Archs
License: DFSG free
Git

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.

Please cite: M. Matsumoto and T. Nishimura: Mersenne Twister: A 623-Dimensionally Equidistributed Uniform Pseudo-Random Number Generator. ACM Transactions on Modeling and Computer Simulation 8(1):3-30 (1998)
Minisat+
solveur de contraintes pseudo booléennes
Versions of package minisat+
ReleaseVersionArchitectures
bullseye1.0-4amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
wheezy1.0-2amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
sid1.0-4amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
jessie1.0-2amd64,armel,armhf,i386
stretch1.0-3amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster1.0-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package minisat+:
fieldmathematics
roleprogram
Popcon: 5 users (2 upd.)*
Versions and Archs
License: DFSG free
Git

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
démonstration automatique de théorèmes
Versions of package mona
ReleaseVersionArchitectures
squeeze1.4-13-1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
buster1.4-17-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch1.4-17-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie1.4-15-1amd64,armel,armhf,i386
wheezy1.4-13-3amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
sid1.4-17-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bullseye1.4-17-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
Debtags of package mona:
fieldmathematics
roleprogram
scopeutility
Popcon: 8 users (2 upd.)*
Versions and Archs
License: DFSG free
Git

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/.

Picosat
solveur SAT avec gestion de démonstrations et « core »
Versions of package picosat
ReleaseVersionArchitectures
stretch960-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie960-1amd64,armel,armhf,i386
wheezy936-4amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
squeeze913-4amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
sid965-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bullseye965-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster960-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package picosat:
fieldmathematics
roleprogram
Popcon: 11 users (0 upd.)*
Versions and Archs
License: DFSG free
Git

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.

Screenshots of package picosat
Proofgeneral
frontal générique d’assistants de preuve
Versions of package proofgeneral
ReleaseVersionArchitectures
sid4.4.1~pre170114-1.1all
jessie4.3~pre131011-0.2all
squeeze3.7-4all
wheezy4.2~pre120605-2all
stretch4.4.1~pre170114-1all
Debtags of package proofgeneral:
fieldmathematics
interfacetext-mode, x11
roleplugin
suiteemacs
useediting
Popcon: 12 users (8 upd.)*
Versions and Archs
License: DFSG free

« 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.)

Other screenshots of package proofgeneral
VersionURL
4.3~pre130510-1.1https://screenshots.debian.net/screenshots/000/012/105/large.png
Screenshots of package proofgeneral
Prover9
démonstrateur de théorème et générateur de contre-exemples
Versions of package prover9
ReleaseVersionArchitectures
squeeze0.0.200902a-2amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
jessie0.0.200911a-2.1amd64,armel,armhf,i386
stretch0.0.200911a-2.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster0.0.200911a-2.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
wheezy0.0.200902a-2.1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
Popcon: 36 users (10 upd.)*
Versions and Archs
License: DFSG free
Bzr

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.

Sat4j
bibliothèque de solveurs SAT en Java
Versions of package sat4j
ReleaseVersionArchitectures
bullseye2.3.5-0.3all
stretch2.3.5-0.2all
jessie2.3.3-1all
squeeze2.2.0-3all
wheezy2.3.1-1all
sid2.3.5-0.3all
buster2.3.5-0.3all
Debtags of package sat4j:
fieldmathematics
roleprogram, shared-lib
Popcon: 209 users (47 upd.)*
Versions and Archs
License: DFSG free

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
démonstrateur automatique de théorème pour la logique du premier ordre avec égalité
Versions of package spass
ReleaseVersionArchitectures
squeeze3.7-2amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
stretch3.7-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid3.7-4amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
wheezy3.7-3amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie3.7-3amd64,armel,armhf,i386
Debtags of package spass:
fieldmathematics
Popcon: 5 users (0 upd.)*
Versions and Archs
License: DFSG free
Git

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
Exact combinatorial optimization for Graphical Models
Versions of package toulbar2
ReleaseVersionArchitectures
buster1.0.0+dfsg3-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye1.0.0+dfsg3-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
sid1.0.0+dfsg3-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
Popcon: 7 users (4 upd.)*
Versions and Archs
License: DFSG free
Git

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
Outil de vérification logicielle
Versions of package why
ReleaseVersionArchitectures
wheezy2.30+dfsg-5amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie2.34-2amd64,armel,armhf,i386
squeeze2.26+dfsg-2+squeeze1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
Debtags of package why:
develtesting-qa
roleprogram
Popcon: 0 users (1 upd.)*
Versions and Archs
License: DFSG free
Git

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.

Screenshots of package why
Why3
plateforme de vérification logicielle
Versions of package why3
ReleaseVersionArchitectures
buster1.2.0-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye1.2.1-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
stretch0.87.3-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid1.2.1-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
Popcon: 9 users (10 upd.)*
Versions and Archs
License: DFSG free
Git

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.

Z3
justificateur de théorème de Microsoft Research
Versions of package z3
ReleaseVersionArchitectures
stretch4.4.1-1~deb9u1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid4.8.7-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bullseye4.8.6-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster4.4.1-1~deb10u1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Popcon: 21 users (38 upd.)*
Versions and Archs
License: DFSG free
Git

Z3 est un justificateur de théorème à la pointe de l’art de Microsoft Research. 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.

Official Debian packages with lower relevance

Coinor-libcoinmp-dev
API C simple pour les solveurs Clp et Cbc de COIN-OR – fichiers de développement
Versions of package coinor-libcoinmp-dev
ReleaseVersionArchitectures
buster1.8.3-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch1.7.6+dfsg1-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie1.7.6+dfsg1-1amd64,armel,armhf,i386
sid1.8.3-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bullseye1.8.3-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
Popcon: 6 users (6 upd.)*
Versions and Archs
License: DFSG free

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.

*Popularitycontest results: number of people who use this package regularly (number of people who upgraded this package recently) out of 202987