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
sid2.6.4.3-1all
trixie2.6.4.3-1all
bookworm2.6.2.2-1.1all
bullseye2.6.1-1all
stretch2.5.1.1-3all
buster2.5.4.1-3all
jessie2.4.0.2-2all
upstream2.7.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
bullseye2.0.0-7amd64,arm64,armel,i386,mips64el,mipsel,ppc64el,s390x
buster2.0.0-3amd64,arm64,i386
stretch1.30-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie0.95.2-3amd64,armel,armhf,i386
Debtags of package alt-ergo:
roleprogram
uitoolkitgtk
Popcon: 1 users (0 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é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
solveur SMT pour les vecteurs de bits et les tableaux
Versions of package boolector
ReleaseVersionArchitectures
buster1.5.118.6b56be4.121013-1amd64,arm64,armhf,i386
stretch1.5.118.6b56be4.121013-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie1.5.118.6b56be4.121013-1amd64,armel,armhf,i386
bullseye1.5.118.6b56be4.121013-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bookworm1.5.118.6b56be4.121013-1.3amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
trixie1.5.118.6b56be4.121013-1.3amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
sid1.5.118.6b56be4.121013-1.3amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
Debtags of package boolector:
roleprogram
Popcon: 2 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
trixie3.3.5-4.2amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
sid3.3.5-4.2amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
bookworm3.3.5-4.2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bullseye3.3.5-4amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster3.3.4-2amd64,arm64,armhf,i386
stretch3.2.1-3amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie3.1.0-1amd64,armel,armhf,i386
Debtags of package clasp:
roleprogram
Popcon: 15 users (11 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).

Please cite: Martin Gebser, Benjamin Kaufmann and Torsten Schaub: Conflict-Driven Answer Set Solving: From Theory to Practice. Artificial Intelligence (187–188):52–89 (2012)
coinor-cbc
solveur de programmes en variables mixtes par branch-and-cut COIN-OR
Versions of package coinor-cbc
ReleaseVersionArchitectures
trixie2.10.12+ds-1amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
bookworm2.10.8+ds1-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bullseye2.10.5+ds1-3amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster2.9.9+repack1-1amd64,arm64,armhf,i386
stretch2.8.12-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie2.8.12-1amd64,armel,armhf,i386
sid2.10.12+ds-1amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
Popcon: 75 users (24 upd.)*
Versions and Archs
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,armhf,i386
bullseye5.6.16+repack1-3amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bookworm5.6.17+dfsg-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
trixie5.6.17+dfsg-1amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
sid5.6.17+dfsg-1amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
jessie5.6.1-1amd64,armel,armhf,i386
stretch5.6.1-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Popcon: 8 users (15 upd.)*
Versions and Archs
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.20.0+dfsg-1amd64,arm64,ppc64el,riscv64,s390x
trixie8.19.1+dfsg-3amd64,arm64,ppc64el,riscv64,s390x
jessie8.4pl4dfsg-1amd64,armel,armhf,i386
stretch8.6-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster8.9.0-1amd64,arm64,armhf,i386
bullseye8.12.0-3amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el
bookworm8.16.1+dfsg-1amd64,arm64,armhf,i386,ppc64el,s390x
Debtags of package coq:
develcompiler
fieldmathematics
interfacecommandline, text-mode
roleprogram
scopeutility
uitoolkitncurses
Popcon: 27 users (21 upd.)*
Versions and Archs
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.

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

The package is enhanced by the following packages: libaac-tactics-ocaml libssreflect-ocaml
cvc4
automated theorem prover for SMT problems
Versions of package cvc4
ReleaseVersionArchitectures
bookworm1.8-3amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
trixie1.8-3amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
sid1.8-3amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
bullseye1.8-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster1.6-2amd64,i386
Popcon: 5 users (2 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
sid5.01-3amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
bookworm5.01-3amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bullseye5.01-3amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster5.01-3amd64,arm64,armhf,i386
stretch5.01-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie3.04-1amd64,armel,armhf,i386
trixie5.01-3amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
Popcon: 1 users (1 upd.)*
Versions and Archs
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.

drat-trim
??? missing short description for package drat-trim :-(
Versions of package drat-trim
ReleaseVersionArchitectures
trixie0.0~git20240428.effa1dc-2amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
sid0.0~git20240428.effa1dc-2amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
Popcon: 0 users (0 upd.)*
Versions and Archs
License: DFSG free
Git
gringo
outils de « grounding » pour des programmes logiques (disjonctifs)
Versions of package gringo
ReleaseVersionArchitectures
stretch5.1.0-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie4.4.0-1amd64,armel,armhf,i386
bullseye5.4.1-3amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster5.3.0-10amd64,arm64,armhf,i386
sid5.6.2-2amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
trixie5.6.2-2amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
bookworm5.4.1-3.1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
upstream5.7.1
Debtags of package gringo:
roleprogram
Popcon: 16 users (10 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
démonstrateur de théorème HOL Light
Versions of package hol-light
ReleaseVersionArchitectures
jessie20131026-1amd64,armel,armhf,i386
sid20231021-2amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
bookworm20230128-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bullseye20190729-4amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
stretch20170109-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Popcon: 0 users (9 upd.)*
Versions and Archs
License: DFSG free
Git

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.

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.19940316dfsg-5amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
buster2.02.19940316-35amd64,arm64,armhf,i386
bullseye2.02.19940316-35.1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bookworm2.02.19940316dfsg-5amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
trixie2.02.19940316dfsg-5amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
stretch2.02.19940316-33amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package hol88:
uitoolkitncurses
Popcon: 0 users (1 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.

kissat
??? missing short description for package kissat :-(
Versions of package kissat
ReleaseVersionArchitectures
sid4.0.1-3amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
trixie4.0.1-3amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
Popcon: 1 users (0 upd.)*
Versions and Archs
License: DFSG free
Git
lbt
Convertit des formules LTL en automates Büchi
Versions of package lbt
ReleaseVersionArchitectures
trixie1.2.2-7amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
sid1.2.2-7amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
bookworm1.2.2-7amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bullseye1.2.2-7amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster1.2.2-6amd64,arm64,armhf,i386
stretch1.2.2-6amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie1.2.2-5amd64,armel,armhf,i386
Debtags of package lbt:
fieldmathematics
interfacecommandline
roleprogram
scopeutility
useconverting
Popcon: 5 users (4 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).

maria
analyseur d'accessibilité pour les réseaux de systèmes algébriques
Versions of package maria
ReleaseVersionArchitectures
jessie1.3.5-4amd64,armel,armhf,i386
sid1.3.5-6amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
trixie1.3.5-6amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
bullseye1.3.5-4.1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bookworm1.3.5-4.1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster1.3.5-4.1amd64,arm64,armhf,i386
stretch1.3.5-4.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package maria:
develtesting-qa
fieldmathematics
interfacetext-mode
roleprogram
scopeutility
uitoolkitncurses
Popcon: 6 users (9 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.

maude
cadriciel logique de haute performance
Versions of package maude
ReleaseVersionArchitectures
sid3.4-1amd64,arm64,mips64el,ppc64el,riscv64,s390x
bullseye3.1-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bookworm3.2-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
stretch2.7-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie2.6-6amd64,armel,armhf,i386
trixie3.4-1amd64,arm64,mips64el,ppc64el,riscv64,s390x
buster2.7-2amd64,arm64,armhf,i386
upstream3.5
Debtags of package maude:
uitoolkitncurses
Popcon: 3 users (1 upd.)*
Newer upstream!
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
sid1.0-5amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
jessie1.0-2amd64,armel,armhf,i386
stretch1.0-3amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster1.0-4amd64,arm64,armhf,i386
bullseye1.0-4amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bookworm1.0-4amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
trixie1.0-5amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
Debtags of package minisat+:
fieldmathematics
roleprogram
Popcon: 3 users (3 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
trixie1.4-18-1amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
buster1.4-17-1amd64,arm64,armhf,i386
bullseye1.4-17-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
stretch1.4-17-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
jessie1.4-15-1amd64,armel,armhf,i386
sid1.4-18-1amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
bookworm1.4-18-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
Debtags of package mona:
fieldmathematics
roleprogram
scopeutility
Popcon: 0 users (1 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
sid965-2amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
jessie960-1amd64,armel,armhf,i386
stretch960-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster960-1amd64,arm64,armhf,i386
bullseye965-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bookworm965-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
trixie965-2amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
Debtags of package picosat:
fieldmathematics
roleprogram
Popcon: 14 users (18 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
stretch4.4.1~pre170114-1all
bullseye4.4.1~pre170114-1.2all
bookworm4.4.1~pre170114-1.2all
sid4.5-2all
jessie4.3~pre131011-0.2all
Debtags of package proofgeneral:
fieldmathematics
interfacetext-mode, x11
roleplugin
suiteemacs
useediting
Popcon: 4 users (9 upd.)*
Versions and Archs
License: DFSG free
Git

« 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.2~pre120605-2 -https://screenshots.debian.net/shrine/screenshot/9621/simage/large-cd932ab2b34519b53b8f75d22359cb9e.png
Screenshots of package proofgeneral
prover9
démonstrateur de théorème et générateur de contre-exemples
Versions of package prover9
ReleaseVersionArchitectures
stretch0.0.200911a-2.1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster0.0.200911a-2.1amd64,arm64,armhf,i386
jessie0.0.200911a-2.1amd64,armel,armhf,i386
Popcon: 7 users (3 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
sid2.3.5-0.3all
trixie2.3.5-0.3all
bookworm2.3.5-0.3all
buster2.3.5-0.3all
Debtags of package sat4j:
fieldmathematics
roleprogram, shared-lib
Popcon: 16 users (6 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
bullseye3.9-1.1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bookworm3.9-1.1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
jessie3.7-3amd64,armel,armhf,i386
stretch3.7-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid3.9-1.1amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
trixie3.9-1.1amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
Debtags of package spass:
fieldmathematics
Popcon: 1 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
bullseye1.1.1+dfsg-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bookworm1.1.1+dfsg-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
sid1.2.1+dfsg-0.1amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
buster1.0.0+dfsg3-2amd64,arm64,armhf,i386
Popcon: 3 users (10 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.

why3
Software verification platform
Versions of package why3
ReleaseVersionArchitectures
trixie1.7.2-2amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
sid1.7.2-2amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
stretch0.87.3-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bullseye1.3.3-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bookworm1.5.1-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster1.2.0-1amd64,arm64,armhf,i386
Popcon: 5 users (1 upd.)*
Versions and Archs
License: DFSG free
Git

Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.). A user can write WhyML programs directly and get correct-by-construction OCaml programs through an automated extraction mechanism. WhyML is also used as an intermediate language for the verification of C, Java, or Ada programs.

Why3 is a complete reimplementation of the former Why platform. Among the new features are: numerous extensions to the input language, a new architecture for calling external provers, and a well-designed API, allowing to use Why3 as a software library. An important emphasis is put on modularity and genericity, giving the end user a possibility to easily reuse Why3 formalizations or to add support for a new external prover if wanted.

z3
theorem prover from Microsoft Research
Versions of package z3
ReleaseVersionArchitectures
stretch4.4.1-1~deb9u1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
sid4.13.3-1amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
buster4.4.1-1~deb10u1amd64,arm64,armhf,i386
bullseye4.8.10-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bookworm4.8.12-3.1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
trixie4.13.3-1amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
Popcon: 10 users (43 upd.)*
Versions and Archs
License: DFSG free
Git

Z3 is a state-of-the-art theorem prover from Microsoft Research. It can be used to check the satisfiability of logical formulas over one or more theories. Z3 offers a compelling match for software analysis and verification tools, since several common software constructs map directly into supported theories.

The Z3 input format is an extension of the one defined by the SMT-LIB 2.0 standard.

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.4+dfsg-2amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64
bullseye1.8.3-3amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
trixie1.8.3-3amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,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,armhf,i386
bookworm1.8.3-3amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
experimental1.8.4+dfsg-1amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
sid1.8.3-3s390x
Popcon: 5 users (24 upd.)*
Versions and Archs
License: DFSG free
Git

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 248069