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
bullseye2.5.4.1-3all
sid2.5.4.1-3all
wheezy2.3.0.1-2all
jessie2.4.0.2-2all
stretch2.5.1.1-3all
buster2.5.4.1-3all
upstream2.6.0.1
Debtags of package agda:
rolemetapackage
Popcon: 0 users (0 upd.)*
Newer upstream!
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
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-4amd64,arm64,armel,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye2.0.0-4amd64,arm64,armel,i386,mips,mips64el,mipsel,ppc64el,s390x
buster2.0.0-3amd64,arm64,armel,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch1.30-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package alt-ergo:
roleprogram
uitoolkitgtk
Popcon: 4 users (15 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
jessie1.5.118.6b56be4.121013-1amd64,armel,armhf,i386
bullseye1.5.118.6b56be4.121013-1amd64,arm64,armel,armhf,i386,mips,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
sid1.5.118.6b56be4.121013-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
wheezy1.4.ffc2089.100608-1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
squeeze1.4.ffc2089.100608-1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
Debtags of package boolector:
roleprogram
Popcon: 2 users (3 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
sid3.3.4-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
wheezy2.0.6-2amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie3.1.0-1amd64,armel,armhf,i386
stretch3.2.1-3amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster3.3.4-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye3.3.4-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package clasp:
roleprogram
Popcon: 84 users (292 upd.)*
Versions and Archs
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
wheezy1.0.1-5amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie1.0.1-5amd64,armel,armhf,i386
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
stretch2.8.12-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid2.9.9+repack1-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye2.9.9+repack1-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster2.9.9+repack1-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie2.8.12-1amd64,armel,armhf,i386
upstream2.10.3
Popcon: 27 users (275 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
sid5.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
buster5.6.16+repack1-1.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye5.6.16+repack1-1.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
upstream5.6.17
Popcon: 15 users (19 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
proof assistant for higher-order logic (toplevel and compiler)
Versions of package coq
ReleaseVersionArchitectures
bullseye8.9.0-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
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
stretch8.6-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster8.9.0-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid8.9.0-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
squeeze8.2.pl2+dfsg-1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
upstream8.9.1
Debtags of package coq:
develcompiler
fieldmathematics
interfacecommandline, text-mode
roleprogram
scopeutility
uitoolkitncurses
Popcon: 32 users (71 upd.)*
Newer upstream!
License: DFSG free
Git

Coq is a proof assistant for higher-order logic, which allows the development of computer programs consistent with their formal specification. It is developed using Objective Caml and Camlp5.

This package provides coqtop, a command line interface to Coq.

The proofgeneral package allows proofs to be edited using Emacs and XEmacs.

The package is enhanced by the following packages: libaac-tactics-ocaml libssreflect-ocaml
Cvc3
démonstrateur automatique de théorème pour les problèmes SMT
Maintainer: Morgan Deters (Adrian Bunk)
Versions of package cvc3
ReleaseVersionArchitectures
sid2.4.1-5.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch2.4.1-5.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie2.4.1-5amd64,armel,armhf,i386
wheezy2.4.1-4amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
squeeze2.2-13amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
Debtags of package cvc3:
interfacecommandline
roleprogram
Popcon: 1 users (1 upd.)*
Versions and Archs
License: DFSG free

CVC3 est un démonstrateur automatique de théorèmes pour des problèmes de SMT (satisfiabilité modulo des théories). Il peut être utilisé pour démontrer la validité (ou, doublement, la satisfaisabilité) de formulations du premier ordre dans un grand nombre de théories logiques intégrées et leurs combinaisons.

CVC3 est la dernière mouture d’une série de démonstrateurs SMT populaires, émanant de l’université de Stanford et son système SVC (Stanford Validity Checker). En particulier, elle s’appuie sur la base de code de CVC Lite, son plus récent prédécesseur. Sa conception de haut niveau suit celle du démonstrateur Sammy.

CVC3 fonctionne avec une version de logique du premier ordre avec des types polymorphes et possède un large éventail de fonctions, dont :

 – plusieurs ensembles de théorèmes de base intégrés : arithmétique
   linéaire des nombres entiers ou rationnels, matrice, n-uplet,
   enregistrement, type de données inductives, tableau de bits et égalité
   avec les symboles de fonction non interprétée ;
 – prise en charge des quantificateurs ;
 – interface interactive basée sur le texte ;
 – interfaces de programmation riches en C, C++ et Java pour embarquer
   d’autres systèmes ;
 – capacités de preuve et modèle ;
 – sous-typage de prédicat ;
 – pratiquement aucune limite pour son utilisation commerciale ou pour la
   recherche (consulter sa licence).

Ce paquet fournit le programme CVC3 en ligne de commande.

The package is enhanced by the following packages: cvc3-el
Cvc4
automated theorem prover for SMT problems
Versions of package cvc4
ReleaseVersionArchitectures
bullseye1.6-2amd64,i386,mips,mips64el,mipsel
buster1.6-2amd64,i386,mips,mips64el,mipsel
sid1.6-2amd64,i386,mips,mips64el,mipsel
Popcon: 3 users (16 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
jessie3.04-1amd64,armel,armhf,i386
wheezy0.1-1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
sid5.01-3amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch5.01-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye5.01-3amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
upstream6.03
Popcon: 5 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
sid5.3.0-10amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye5.3.0-10amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
wheezy3.0.4-3amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
stretch5.1.0-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie4.4.0-1amd64,armel,armhf,i386
buster5.3.0-10amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package gringo:
roleprogram
Popcon: 88 users (293 upd.)*
Versions and Archs
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,mips,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
bullseye20190729-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Popcon: 3 users (3 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
jessie2.02.19940316-28amd64,armel,armhf,i386
sid2.02.19940316-35amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch2.02.19940316-33amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
wheezy2.02.19940316-15amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
squeeze2.02.19940316-13.1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
buster2.02.19940316-35amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye2.02.19940316-35amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package hol88:
uitoolkitncurses
Popcon: 1 users (8 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,mips,mips64el,mipsel,ppc64el,s390x
squeeze1.2.2-4amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy1.2.2-5amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,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,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package lbt:
fieldmathematics
interfacecommandline
roleprogram
scopeutility
useconverting
Popcon: 8 users (6 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
sid1.3.5-4.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye1.3.5-4.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster1.3.5-4.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch1.3.5-4.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie1.3.5-4amd64,armel,armhf,i386
wheezy1.3.5-4amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
squeeze1.3.5-2amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
Debtags of package maria:
develtesting-qa
fieldmathematics
interfacetext-mode
roleprogram
scopeutility
uitoolkitncurses
Popcon: 10 users (18 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,mips,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 (3 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
buster2.7-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye2.7-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid2.7-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
wheezy2.6-2amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
stretch2.7-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package maude:
uitoolkitncurses
Popcon: 4 users (4 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
stretch1.0-3amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid1.0-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye1.0-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster1.0-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
wheezy1.0-2amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie1.0-2amd64,armel,armhf,i386
Debtags of package minisat+:
fieldmathematics
roleprogram
Popcon: 3 users (4 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
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
squeeze1.4-13-1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
sid1.4-17-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye1.4-17-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package mona:
fieldmathematics
roleprogram
scopeutility
Popcon: 3 users (8 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 »
Maintainer: Michael Tautschnig
Versions of package picosat
ReleaseVersionArchitectures
jessie960-1amd64,armel,armhf,i386
squeeze913-4amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
sid960-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye960-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster960-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
stretch960-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
wheezy936-4amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
upstream965
Debtags of package picosat:
fieldmathematics
roleprogram
Popcon: 6 users (1 upd.)*
Newer upstream!
License: DFSG free

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
stretch4.4.1~pre170114-1all
squeeze3.7-4all
bullseye4.4.1~pre170114-1.1all
wheezy4.2~pre120605-2all
jessie4.3~pre131011-0.2all
sid4.4.1~pre170114-1.1all
Debtags of package proofgeneral:
fieldmathematics
interfacetext-mode, x11
roleplugin
suiteemacs
useediting
Popcon: 24 users (16 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
bullseye0.0.200911a-2.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
squeeze0.0.200902a-2amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy0.0.200902a-2.1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,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
sid0.0.200911a-2.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Popcon: 31 users (16 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
sid2.3.5-0.3all
buster2.3.5-0.3all
stretch2.3.5-0.2all
jessie2.3.3-1all
squeeze2.2.0-3all
wheezy2.3.1-1all
Debtags of package sat4j:
fieldmathematics
roleprogram, shared-lib
Popcon: 244 users (97 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
jessie3.7-3amd64,armel,armhf,i386
sid3.7-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
wheezy3.7-3amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
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
Debtags of package spass:
fieldmathematics
Popcon: 2 users (1 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
sid1.0.0+dfsg3-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye1.0.0+dfsg3-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Popcon: 10 users (17 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
squeeze2.26+dfsg-2+squeeze1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
jessie2.34-2amd64,armel,armhf,i386
Debtags of package why:
develtesting-qa
roleprogram
Popcon: 1 users (0 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
stretch0.87.3-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid1.2.0-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye1.2.0-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster1.2.0-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Popcon: 2 users (12 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-0.4~deb9u1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster4.4.1-0.4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye4.4.1-0.4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid4.4.1-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
upstream4.8.4
Popcon: 14 users (16 upd.)*
Newer upstream!
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
sid1.8.3-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie1.7.6+dfsg1-1amd64,armel,armhf,i386
stretch1.7.6+dfsg1-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster1.8.3-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye1.8.3-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Popcon: 4 users (9 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 196492