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 |
Release | Version | Architectures |
trixie | 2.6.4.3-1 | all |
bullseye | 2.6.1-1 | all |
jessie | 2.4.0.2-2 | all |
stretch | 2.5.1.1-3 | all |
buster | 2.5.4.1-3 | all |
sid | 2.6.4.3-1 | all |
bookworm | 2.6.2.2-1.1 | all |
upstream | 2.7.0.1 |
Debtags of package agda: |
role | metapackage |
|
License: DFSG free
|
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 |
Release | Version | Architectures |
buster | 2.0.0-3 | amd64,arm64,i386 |
bullseye | 2.0.0-7 | amd64,arm64,armel,i386,mips64el,mipsel,ppc64el,s390x |
jessie | 0.95.2-3 | amd64,armel,armhf,i386 |
stretch | 1.30-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
Debtags of package alt-ergo: |
role | program |
uitoolkit | gtk |
|
License: DFSG free
|
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 |
Release | Version | Architectures |
bookworm | 1.5.118.6b56be4.121013-1.3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
sid | 1.5.118.6b56be4.121013-1.3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
trixie | 1.5.118.6b56be4.121013-1.3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
jessie | 1.5.118.6b56be4.121013-1 | amd64,armel,armhf,i386 |
stretch | 1.5.118.6b56be4.121013-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
buster | 1.5.118.6b56be4.121013-1 | amd64,arm64,armhf,i386 |
bullseye | 1.5.118.6b56be4.121013-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
Debtags of package boolector: |
role | program |
|
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 |
Release | Version | Architectures |
trixie | 3.3.5-4.2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
bookworm | 3.3.5-4.2 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bullseye | 3.3.5-4 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
buster | 3.3.4-2 | amd64,arm64,armhf,i386 |
stretch | 3.2.1-3 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
jessie | 3.1.0-1 | amd64,armel,armhf,i386 |
sid | 3.3.5-4.2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
Debtags of package clasp: |
role | program |
|
License: DFSG free
|
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).
|
|
coinor-cbc
solveur de programmes en variables mixtes par branch-and-cut COIN-OR
|
Versions of package coinor-cbc |
Release | Version | Architectures |
sid | 2.10.12+ds-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
bookworm | 2.10.8+ds1-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
buster | 2.9.9+repack1-1 | amd64,arm64,armhf,i386 |
jessie | 2.8.12-1 | amd64,armel,armhf,i386 |
bullseye | 2.10.5+ds1-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
stretch | 2.8.12-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
trixie | 2.10.12+ds-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
|
License: DFSG free
|
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 |
Release | Version | Architectures |
jessie | 5.6.1-1 | amd64,armel,armhf,i386 |
sid | 5.6.17+dfsg-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
trixie | 5.6.17+dfsg-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
bookworm | 5.6.17+dfsg-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bullseye | 5.6.16+repack1-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
buster | 5.6.16+repack1-1.1 | amd64,arm64,armhf,i386 |
stretch | 5.6.1-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
|
License: DFSG free
|
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 |
Release | Version | Architectures |
sid | 8.19.1+dfsg-3 | amd64,arm64,ppc64el,riscv64,s390x |
trixie | 8.19.1+dfsg-3 | amd64,arm64,ppc64el,riscv64,s390x |
stretch | 8.6-4 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
bookworm | 8.16.1+dfsg-1 | amd64,arm64,armhf,i386,ppc64el,s390x |
jessie | 8.4pl4dfsg-1 | amd64,armel,armhf,i386 |
bullseye | 8.12.0-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el |
buster | 8.9.0-1 | amd64,arm64,armhf,i386 |
upstream | 8.20.0 |
Debtags of package coq: |
devel | compiler |
field | mathematics |
interface | commandline, text-mode |
role | program |
scope | utility |
uitoolkit | ncurses |
|
License: DFSG free
|
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é.
|
|
cvc4
automated theorem prover for SMT problems
|
Versions of package cvc4 |
Release | Version | Architectures |
trixie | 1.8-3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
buster | 1.6-2 | amd64,i386 |
bullseye | 1.8-2 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 1.8-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
sid | 1.8-3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
|
License: DFSG free
|
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 |
Release | Version | Architectures |
sid | 5.01-3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
jessie | 3.04-1 | amd64,armel,armhf,i386 |
trixie | 5.01-3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
bookworm | 5.01-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bullseye | 5.01-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
buster | 5.01-3 | amd64,arm64,armhf,i386 |
stretch | 5.01-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
|
License: DFSG free
|
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 |
Release | Version | Architectures |
trixie | 0.0~git20240428.effa1dc-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
sid | 0.0~git20240428.effa1dc-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
|
License: DFSG free
|
|
|
gringo
outils de « grounding » pour des programmes logiques (disjonctifs)
|
Versions of package gringo |
Release | Version | Architectures |
stretch | 5.1.0-4 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
jessie | 4.4.0-1 | amd64,armel,armhf,i386 |
bullseye | 5.4.1-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
buster | 5.3.0-10 | amd64,arm64,armhf,i386 |
sid | 5.6.2-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
trixie | 5.6.2-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
bookworm | 5.4.1-3.1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
upstream | 5.7.1 |
Debtags of package gringo: |
role | program |
|
License: DFSG free
|
La solution actuelle fixe les solveurs pour œuvrer sur des programmes avec
des variables libres. Par conséquent, un « grounder » (ancrage
situationnel) est nécessaire, qui, un programme d’entrée étant indiqué avec
des variables de premier ordre, calcule le programme « ground » équivalent
(variables libres).
Ce paquet fournit les outils suivants :
– gringo : un grounder qui, un programme d’entrée étant indiqué avec des
variables de premier ordre, calcule le programme « ground » équivalent
(variables libres) au format aspif. Sa sortie peut être traitée plus
tard avec clasp, un solveur « answer set » (programmation déclarative).
À partir des séries cinq de gringo, la sortie de celui-ci n’est plus
directement compatible avec les solveurs tels smodels ou cmodels lisant
le format smodels. Lpconvert est à utiliser pour convertir le format
aspif au format smodels ;
– clingo : une combinaison de gringo et clasp dans un système
monolithique. De cette façon, il propose plus de contrôle sur les
traitements de grounding et de résolution que gringo et clasp peuvent
proposer individuellement : la résolution à répétition ;
– lpconvert : un convertisseur entre les formats aspif de gringo et
smodels ;
– reify : un petit utilitaire qui réifie les programmes logiques donnés
au format aspif. Il produit un ensemble d’éléments pouvant être traités
ultérieurement avec gringo.
|
|
hol-light
démonstrateur de théorème HOL Light
|
Versions of package hol-light |
Release | Version | Architectures |
jessie | 20131026-1 | amd64,armel,armhf,i386 |
sid | 20231021-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
bookworm | 20230128-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bullseye | 20190729-4 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
stretch | 20170109-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
|
License: DFSG free
|
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
|
Versions of package hol88 |
Release | Version | Architectures |
jessie | 2.02.19940316-28 | amd64,armel,armhf,i386 |
sid | 2.02.19940316dfsg-5 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
buster | 2.02.19940316-35 | amd64,arm64,armhf,i386 |
bullseye | 2.02.19940316-35.1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 2.02.19940316dfsg-5 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
trixie | 2.02.19940316dfsg-5 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
stretch | 2.02.19940316-33 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
Debtags of package hol88: |
uitoolkit | ncurses |
|
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 |
Release | Version | Architectures |
sid | 4.0.1-3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
trixie | 4.0.1-3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
|
License: DFSG free
|
|
|
lbt
Convertit des formules LTL en automates Büchi
|
Versions of package lbt |
Release | Version | Architectures |
trixie | 1.2.2-7 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
sid | 1.2.2-7 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
bookworm | 1.2.2-7 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bullseye | 1.2.2-7 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
buster | 1.2.2-6 | amd64,arm64,armhf,i386 |
stretch | 1.2.2-6 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
jessie | 1.2.2-5 | amd64,armel,armhf,i386 |
Debtags of package lbt: |
field | mathematics |
interface | commandline |
role | program |
scope | utility |
use | converting |
|
License: DFSG free
|
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 |
Release | Version | Architectures |
jessie | 1.3.5-4 | amd64,armel,armhf,i386 |
sid | 1.3.5-6 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
trixie | 1.3.5-6 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
bullseye | 1.3.5-4.1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 1.3.5-4.1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
buster | 1.3.5-4.1 | amd64,arm64,armhf,i386 |
stretch | 1.3.5-4.1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
Debtags of package maria: |
devel | testing-qa |
field | mathematics |
interface | text-mode |
role | program |
scope | utility |
uitoolkit | ncurses |
|
License: DFSG free
|
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 |
Release | Version | Architectures |
sid | 3.4-1 | amd64,arm64,mips64el,ppc64el,riscv64,s390x |
bullseye | 3.1-2 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 3.2-2 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
stretch | 2.7-2 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
jessie | 2.6-6 | amd64,armel,armhf,i386 |
trixie | 3.4-1 | amd64,arm64,mips64el,ppc64el,riscv64,s390x |
buster | 2.7-2 | amd64,arm64,armhf,i386 |
upstream | 3.5 |
Debtags of package maude: |
uitoolkit | ncurses |
|
License: DFSG free
|
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.
|
|
minisat+
solveur de contraintes pseudo booléennes
|
Versions of package minisat+ |
Release | Version | Architectures |
sid | 1.0-5 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
jessie | 1.0-2 | amd64,armel,armhf,i386 |
stretch | 1.0-3 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
buster | 1.0-4 | amd64,arm64,armhf,i386 |
bullseye | 1.0-4 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 1.0-4 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
trixie | 1.0-5 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
Debtags of package minisat+: |
field | mathematics |
role | program |
|
License: DFSG free
|
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 |
Release | Version | Architectures |
trixie | 1.4-18-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
buster | 1.4-17-1 | amd64,arm64,armhf,i386 |
bullseye | 1.4-17-2 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
stretch | 1.4-17-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
jessie | 1.4-15-1 | amd64,armel,armhf,i386 |
sid | 1.4-18-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
bookworm | 1.4-18-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
Debtags of package mona: |
field | mathematics |
role | program |
scope | utility |
|
License: DFSG free
|
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 |
Release | Version | Architectures |
sid | 965-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
jessie | 960-1 | amd64,armel,armhf,i386 |
stretch | 960-1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
buster | 960-1 | amd64,arm64,armhf,i386 |
bullseye | 965-2 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 965-2 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
trixie | 965-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
Debtags of package picosat: |
field | mathematics |
role | program |
|
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.
|
|
proofgeneral
frontal générique d’assistants de preuve
|
Versions of package proofgeneral |
Release | Version | Architectures |
stretch | 4.4.1~pre170114-1 | all |
bullseye | 4.4.1~pre170114-1.2 | all |
bookworm | 4.4.1~pre170114-1.2 | all |
sid | 4.5-2 | all |
jessie | 4.3~pre131011-0.2 | all |
Debtags of package proofgeneral: |
field | mathematics |
interface | text-mode, x11 |
role | plugin |
suite | emacs |
use | editing |
|
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.)
|
|
prover9
démonstrateur de théorème et générateur de contre-exemples
|
Versions of package prover9 |
Release | Version | Architectures |
stretch | 0.0.200911a-2.1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
buster | 0.0.200911a-2.1 | amd64,arm64,armhf,i386 |
jessie | 0.0.200911a-2.1 | amd64,armel,armhf,i386 |
|
License: DFSG free
|
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 |
Release | Version | Architectures |
bullseye | 2.3.5-0.3 | all |
stretch | 2.3.5-0.2 | all |
jessie | 2.3.3-1 | all |
sid | 2.3.5-0.3 | all |
trixie | 2.3.5-0.3 | all |
bookworm | 2.3.5-0.3 | all |
buster | 2.3.5-0.3 | all |
Debtags of package sat4j: |
field | mathematics |
role | program, shared-lib |
|
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 |
Release | Version | Architectures |
bullseye | 3.9-1.1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 3.9-1.1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
jessie | 3.7-3 | amd64,armel,armhf,i386 |
stretch | 3.7-4 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
sid | 3.9-1.1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
trixie | 3.9-1.1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
Debtags of package spass: |
field | mathematics |
|
License: DFSG free
|
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 |
Release | Version | Architectures |
bullseye | 1.1.1+dfsg-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 1.1.1+dfsg-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
sid | 1.2.1+dfsg-0.1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
buster | 1.0.0+dfsg3-2 | amd64,arm64,armhf,i386 |
|
License: DFSG free
|
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 |
Release | Version | Architectures |
trixie | 1.7.2-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
sid | 1.7.2-2 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
stretch | 0.87.3-2 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
bullseye | 1.3.3-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 1.5.1-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
buster | 1.2.0-1 | amd64,arm64,armhf,i386 |
|
License: DFSG free
|
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 |
Release | Version | Architectures |
stretch | 4.4.1-1~deb9u1 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
sid | 4.13.3-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
buster | 4.4.1-1~deb10u1 | amd64,arm64,armhf,i386 |
bullseye | 4.8.10-1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 4.8.12-3.1 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
trixie | 4.13.3-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
|
License: DFSG free
|
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 |
Release | Version | Architectures |
buster | 1.8.3-2 | amd64,arm64,armhf,i386 |
jessie | 1.7.6+dfsg1-1 | amd64,armel,armhf,i386 |
trixie | 1.8.3-3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
experimental | 1.8.4+dfsg-1 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
sid | 1.8.3-3 | amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x |
bullseye | 1.8.3-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
bookworm | 1.8.3-3 | amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x |
stretch | 1.7.6+dfsg1-2 | amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x |
|
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.
|
|
|