Debian Science Project
Summary
Logic
Debian Science - Logik-Pakete

Dieses Metapaket ist Teil des Debian Pure Blends »Debian Science« und installiert Pakete mit Bezug zur Computational Logic. Es enthält Werkzeuge zur Umformung von Formeln und zur Lösung von Formeln für verschiedene Logiken, interaktive Beweissysteme (proof systems) usw.

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
Abhängig typisierte, funktionale Programmiersprache
Versions of package agda
ReleaseVersionArchitectures
trixie2.6.4.3-1all
bullseye2.6.1-1all
jessie2.4.0.2-2all
stretch2.5.1.1-3all
buster2.5.4.1-3all
sid2.6.4.3-1all
bookworm2.6.2.2-1.1all
upstream2.7.0.1
Debtags of package agda:
rolemetapackage
Popcon: 0 users (0 upd.)*
Newer upstream!
License: DFSG free
Git

Agda ist eine abhängig typisierte, funktionale Programmiersprache: Sie besitzt induktive Familien, die wie Haskells GADTs sind, jedoch mit Werten und nicht nur mit Typen indiziert werden können. Zusätzlich besitzt sie parametrisierte Module, mixfix-Operatoren, Unicode-Kodierung und eine interaktive Emacs-Schnittstelle (die Typüberprüfung kann bei der Codeentwicklung hilfreich sein).

Agda ist auch ein Beweisassistent, ein interaktives System zum Schreiben und Überprüfen von Beweisen. Agda basiert auf der intuitionistischen Typentheorie, einem grundlegenden System für konstruktive Mathematik, entwickelt vom schwedischen Logiker Per Martin-Löf. Es ähnelt anderen Beweisassistenten, die auf abhängigen Typen basieren, wie Coq, Epigram und NuPRL.

Dieses Metapaket liefert den Emacs-Modus, die ausführbare Anwendung, die Standardbibliothek und die Dokumentation für Agda.

alt-ergo
Automatic theorem prover dedicated to program verification
Versions of package alt-ergo
ReleaseVersionArchitectures
buster2.0.0-3amd64,arm64,i386
bullseye2.0.0-7amd64,arm64,armel,i386,mips64el,mipsel,ppc64el,s390x
jessie0.95.2-3amd64,armel,armhf,i386
stretch1.30-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Debtags of package alt-ergo:
roleprogram
uitoolkitgtk
Popcon: 0 users (0 upd.)*
Versions and Archs
License: DFSG free
Git

Alt-Ergo is an automatic theorem prover geared towards application in program verification. It is based on CC(X), a congruence closure algorithm parameterized by an equational theory X. Alt-Ergo has built-in provers for propositional logic, linear arithmetic, uninterpreted function symbols, associative-commutative function symbols, polymorphic arrays, user-defined polymorphic record types and polymorphic enumeration types. It has restricted support for reasoning over arbitrary user-defined algebraic types, first-order quantifiers, and non-linear arithmetic.

This package contains the prover as a command-line executable.

boolector
SMT-Solver für Bit-Vektoren und Arrays
Versions of package boolector
ReleaseVersionArchitectures
bookworm1.5.118.6b56be4.121013-1.3amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
sid1.5.118.6b56be4.121013-1.3amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
trixie1.5.118.6b56be4.121013-1.3amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
jessie1.5.118.6b56be4.121013-1amd64,armel,armhf,i386
stretch1.5.118.6b56be4.121013-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
buster1.5.118.6b56be4.121013-1amd64,arm64,armhf,i386
bullseye1.5.118.6b56be4.121013-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
Debtags of package boolector:
roleprogram
Popcon: 1 users (1 upd.)*
Versions and Archs
License: DFSG free

Boolector ist ein effizienter SMT-Löser für die quantifiziererfreie Theorie von Bitvektoren in Kombination mit der quantifiziererfreien Extensionstheorie von Arrays.

clasp
conflict-driven nogood learning answer set solver
Versions of package clasp
ReleaseVersionArchitectures
trixie3.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
sid3.3.5-4.2amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
Debtags of package clasp:
roleprogram
Popcon: 13 users (12 upd.)*
Versions and Archs
License: DFSG free
Git

clasp is an answer set solver for (extended) normal logic programs. It combines the high-level modeling capacities of answer set programming (ASP) with state-of-the-art techniques from the area of Boolean constraint solving. The primary clasp algorithm relies on conflict-driven nogood learning, a technique that proved very successful for satisfiability checking (SAT). Unlike other learning ASP solvers, clasp does not rely on legacy software, such as a SAT solver or any other existing ASP solver. Rather, clasp has been genuinely developed for answer set solving based on conflict-driven nogood learning. clasp can be applied as an ASP solver (on LPARSE output format), as a SAT solver (on simplified DIMACS/CNF format), or as a PB solver (on OPB format).

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
Coin-or branch-and-cut mixed integer programming solver
Versions of package coinor-cbc
ReleaseVersionArchitectures
sid2.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
buster2.9.9+repack1-1amd64,arm64,armhf,i386
jessie2.8.12-1amd64,armel,armhf,i386
bullseye2.10.5+ds1-3amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
stretch2.8.12-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
trixie2.10.12+ds-1amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
Popcon: 73 users (22 upd.)*
Versions and Archs
License: DFSG free
Git

Cbc (Coin-or branch and cut) is an open-source mixed integer programming solver written in C++. It can be used as a callable library or as a stand-alone executable.

This package contains cbc executable.

coinor-symphony
COIN-OR solver for mixed-integer linear programs
Versions of package coinor-symphony
ReleaseVersionArchitectures
jessie5.6.1-1amd64,armel,armhf,i386
sid5.6.17+dfsg-1amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
trixie5.6.17+dfsg-1amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
bookworm5.6.17+dfsg-1amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bullseye5.6.16+repack1-3amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
buster5.6.16+repack1-1.1amd64,arm64,armhf,i386
stretch5.6.1-1amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Popcon: 6 users (21 upd.)*
Versions and Archs
License: DFSG free
Git

SYMPHONY is an open-source generic mixed-integer linear programs (MILP) solver, callable library, and extensible framework for implementing customized solvers SYMPHONY has a number of advanced capabilities, including the ability to solve multi-objective MILPs, the ability to warm start its solution procedure, and the ability to perform basic sensitivity analyses.

SYMPHONY is part of the larger COIN-OR initiative (Computational Infrastructure for Operations Research).

This package contains the symphony executable.

coq
Beweis-Assistent für Logik höherer Ordnung (Toplevel und Compiler)
Versions of package coq
ReleaseVersionArchitectures
sid8.19.1+dfsg-3amd64,arm64,ppc64el,riscv64,s390x
trixie8.19.1+dfsg-3amd64,arm64,ppc64el,riscv64,s390x
stretch8.6-4amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
bookworm8.16.1+dfsg-1amd64,arm64,armhf,i386,ppc64el,s390x
jessie8.4pl4dfsg-1amd64,armel,armhf,i386
bullseye8.12.0-3amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el
buster8.9.0-1amd64,arm64,armhf,i386
upstream8.20.0
Debtags of package coq:
develcompiler
fieldmathematics
interfacecommandline, text-mode
roleprogram
scopeutility
uitoolkitncurses
Popcon: 26 users (22 upd.)*
Newer upstream!
License: DFSG free
Git

Coq ist ein Beweis-Assistent für Logik höherer Ordnung. Er ermöglicht die Entwicklung von Computerprogrammen, die konsistent mit ihrer formalen Spezifikation sind. Er wird mittels Objective Caml und Camlp5 entwickelt.

Dieses Paket enthält coqtop, eine Befehlszeilen-Schnittstelle zu Coq.

Eine grafische Oberfläche für Coq finden Sie im Paket coqide. Coq kann auch mit ProofGeneral verwendet werden, was die Bearbeitung der Beweise mit Emacs und XEmacs ermöglicht. Dies erfordert die Installation des Pakets proofgeneral.

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
trixie1.8-3amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
buster1.6-2amd64,i386
bullseye1.8-2amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bookworm1.8-3amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
sid1.8-3amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
Popcon: 4 users (3 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
jessie3.04-1amd64,armel,armhf,i386
trixie5.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
Popcon: 0 users (0 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 (1 upd.)*
Versions and Archs
License: DFSG free
Git
gringo
»grounding tools« für (disjunktive) Logikprogramme
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: 17 users (12 upd.)*
Newer upstream!
License: DFSG free
Git

Aktuelle Programme zur Ermittlung von Antwortmengen (»answer set solvers«) arbeiten mit variablenfreien Programmen. Daher wird ein »Grounder« benötigt, der bei einem gegebenen Eingabeprogramm mit Variablen erster Ordnung ein äquivalentes variablenfreies »ground program« berechnet.

Dieses Paket enthält die folgenden Tools:

  • gringo: ein Grounder, der bei einem gegebenen Eingabeprogramm mit

    Variablen erster Ordnung ein äquivalentes (variablenfreies) ground program im aspif-Format berechnet. Seine Ausgabe kann mit dem answer set solver clasp weiterverarbeitet werden. Beginnend mit der Gringo-Serie 5 ist die Ausgabe nicht mehr direkt mit Solvern wie smodels oder cmodels kompatibel, die das smodels-Format lesen. Verwenden Sie lpconvert zum Übersetzen des aspif-Formats in das smodels-Format. - clingo: kombiniert gringo und clasp zu einem monolithischen System.

    Auf diese Weise bietet es mehr Kontrolle über den Grounding- und Lösungsprozess, als gringo und clasp einzeln bieten können: Multi-Shot-Lösung. - lpconvert: Umwandler für die gringo-Formate aspif und smodels - reify: kleines Dienstprogramm, das Logikprogramme im aspif-Format

    reifiziert (vergegenständlicht). Es erzeugt eine Reihe von Fakten, die mit gringo weiterverarbeitet werden können.

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
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 (5 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
Logik höherer Ordnung - Systemabbild
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

Das HOL-System ist eine Umgebung für interaktives Beweisen von Theoremen in einer Logik höherer Ordnung. Seine herausragendste Eigenschaft ist seine Programmierbarkeit mit der Meta-Sprache ML. Das System hat eine Vielzahl von Verwendungen von der Formalisierung reiner Mathematik bis zur Überprüfung industrieller Hardware. Weltweit arbeiten akademische und industrielle Einrichtungen mit HOL.

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 (1 upd.)*
Versions and Archs
License: DFSG free
Git
lbt
Konvertiert LTL-Formeln zu Büchi-Automaten
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: 4 users (5 upd.)*
Versions and Archs
License: DFSG free
Git

Diese Software konvertiert eine lineare temporäre Logik (ltl)-Formel in einen allgemeinen Büchi-Automaten. Der resultierende Automat kann zum Beispiel in Modelltests verwendet werden, wo er die Eigenschaft darstellt, die in dem Modell überprüft wird (z.B. ein Petri-Netz).

maria
Erreichbarkeitsanalyse für Netze algebraischer Systeme
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 (7 upd.)*
Versions and Archs
License: DFSG free
Git

Maria ist ein leistungsfähiges Werkzeug, das entworfen wurde, um Ingenieuren bei der Modellierung und Lösung nebenläufiger Probleme in parallelen und verteilten Computersystemen zu helfen.

Maria findet (gegenseitige) Blockaden (Deadlocks) und Verstöße gegen die Sicherheit oder die garantierten Reaktionszeiten, indem es alle Zustände, die vom Ausgangszustand des Systems erreicht werden können, untersucht. Das Werkzeug verwaltet Dutzende oder Hunderte von Millionen erreichbarer Zustände und aktivierter Aktionen.

Die beeindruckende Kraft von Marias Formalismus nähert sich dank seines großen Systems von Datentypen und leistungsfähigen algebraischen Operationen der von höheren Programmiersprachen.

maude
high-performance logical framework
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 (2 upd.)*
Newer upstream!
License: DFSG free
Git

Maude is a high-performance reflective language and system supporting both equational and rewriting logic specification and programming for a wide range of applications. Maude has been influenced in important ways by the OBJ3 language, which can be regarded as an equational logic sublanguage. Besides supporting equational specification and programming, Maude also supports rewriting logic computation.

Rewriting logic is a logic of concurrent change that can naturally deal with state and with concurrent computations. It has good properties as a general semantic framework for giving executable semantics to a wide range of languages and models of concurrency. In particular, it supports very well concurrent object-oriented computation. The same reasons making rewriting logic a good semantic framework make it also a good logical framework, that is, a metalogic in which many other logics can be naturally represented and executed.

Maude supports in a systematic and efficient way logical reflection. This makes Maude remarkably extensible and powerful, supports an extensible algebra of module composition operations, and allows many advanced metaprogramming and metalanguage applications. Indeed, some of the most interesting applications of Maude are metalanguage applications, in which Maude is used to create executable environments for different logics, theorem provers, languages, and models of computation.

Maude is of interest to the biomedical community for modeling and analysis of biological systems.

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+
solver for pseudo-Boolean constraints
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: 4 users (4 upd.)*
Versions and Archs
License: DFSG free
Git

MinSat+ is a solver for Pseudo-Boolean Optimization (AKA 0-1 integer programming) that is based on the MiniSat SAT-solver. It supports optimizing a linear objective function, subject to a set of linear constraints. The variables of the objective function and constraints are boolean, i.e. required to be 0 or 1. Pseudo-Boolean optimization can be used to solve many kinds of combinatorial optimization problems. This version of Minisat+ is compiled with bignum support for constraint coefficients.

mona
Theorem-Beweiser auf Grundlage von Automaten
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: 1 users (1 upd.)*
Versions and Archs
License: DFSG free
Git

Das Werkzeug MONA übersetzt in den Logiken WS1S oder WS2S beschriebene Formeln in endliche Zustandsautomaten, die mit BDDs dargestellt werden. Die Formeln können Suchmuster, zeitlichen Eigenschaften reaktiver Systeme, Bedingungen von Parse-Bäumen usw. darstellen. MONA untersucht die resultierenden Automaten und stellt fest, ob die Formel gültig ist. Wenn die Formel nicht gültig ist, erzeugt MONA ein Gegenbeispiel.

Dokumentation finden Sie auf der Website von MONA: http://www.brics.dk/mona/.

picosat
SAT solver with proof and core support
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: 15 users (15 upd.)*
Versions and Archs
License: DFSG free
Git

Despite the NP completeness of the satisfiabilty problem of Boolean formulas (SAT), SAT solvers are often able to decide this problem in a reasonable time frame. As all other NP complete problems are reducible to SAT, the solvers have become a general purpose tool for this class of problems.

PicoSAT is a SAT solver that turned out to be faster on industrial instances than MiniSAT 2.0 and also can generate proofs and cores in memory.

Screenshots of package picosat
proofgeneral
Generisches Frontend für Beweisassistenten
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: 6 users (4 upd.)*
Versions and Archs
License: DFSG free
Git

Der »Major Mode« Proof General verwandelt Emacs in einen interaktiven Beweisassistenten, um mithilfe verschiedener Theorembeweiser formale mathematische Beweise zu schreiben.

Mit diesem Paket unterstützt Proof General Coq. (Es gibt keinen anderen Beweisassistenten, den man sinnvoll unterstützen kann.)

Other screenshots of package proofgeneral
VersionURL
4.3~pre130510-1.1https://screenshots.debian.net/shrine/screenshot/12105/simage/large-07f40b860f3c7901980bff73dcb7a431.png
Screenshots of package proofgeneral
prover9
theorem prover and countermodel generator
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 (6 upd.)*
Versions and Archs
License: DFSG free
Bzr

This package provides the Prover9 resolution/paramodulation theorem prover and the Mace4 countermodel generator.

Prover9 is an automated theorem prover for first-order and equational logic. It is a successor of the Otter prover. Prover9 uses the inference techniques of ordered resolution and paramodulation with literal selection.

The program Mace4 searches for finite structures satisfying first-order and equational statements, the same kind of statement that Prover9 accepts. If the statement is the denial of some conjecture, any structures found by Mace4 are counterexamples to the conjecture.

Mace4 can be a valuable complement to Prover9, looking for counterexamples before (or at the same time as) using Prover9 to search for a proof. It can also be used to help debug input clauses and formulas for Prover9.

sat4j
Effiziente Bibliothek aus SAT-Solvern in 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: 14 users (1 upd.)*
Versions and Archs
License: DFSG free

Das Ziel der Bibliothek SAT4J ist es eine effiziente Bibliothek aus SAT-Solvern in Java bereitzustellen. Verglichen mit dem Projekt OpenSAT zielt die Bibliothek SAT4J auf Erstbenutzer von SAT-»Black Boxes« ab, die SAT-Techniken in ihre Anwendungen integrieren wollen ohne sich um die Details zu kümmern. Das Projekt SAT4J versucht darüber hinaus, SAT-Forschern eine Arbeitsgrundlage zu bieten.

spass
automated theorem prover for first-order logic with equality
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 (0 upd.)*
Versions and Archs
License: DFSG free
Git

SPASS is a saturation-based automated theorem prover for first-order logic with equality. It is unique due to the combination of the superposition calculus with specific inference/reduction rules for sorts (types) and a splitting rule for case analysis motivated by the beta-rule of analytic tableaux and the case analysis employed in the Davis-Putnam procedure. Furthermore, SPASS provides a sophisticated clause normal form translation.

This package consists of the SPASS/FLOTTER binary, documentation, and a small example collection. The tools collections contain the proof checker pcs, the syntax translators dfg2otter and dfg2tptp, and the ASCII pretty printer 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 (5 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 (3 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
Theorembeweiser von 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: 6 users (38 upd.)*
Versions and Archs
License: DFSG free
Git

Z3 ist ein hochmoderner Theorembeweiser von Microsoft Research. Er kann verwendet werden, um die Erfüllbarkeit logischer Formeln über eine oder mehrere Theorien zu überprüfen. Z3 bietet eine überzeugende Übereinstimmung mit Softwareanalyse- und Verifizierungswerkzeugen, da mehrere gängige Softwarekonstrukte direkt in unterstützte Theorien abgebildet werden.

Das Z3-Eingabeformat ist eine Erweiterung des vom Standard SMT-LIB 2.0 definierten Formats.

Official Debian packages with lower relevance

coinor-libcoinmp-dev
Simple C API for COIN-OR Solvers Clp and Cbc -- development
Versions of package coinor-libcoinmp-dev
ReleaseVersionArchitectures
buster1.8.3-2amd64,arm64,armhf,i386
jessie1.7.6+dfsg1-1amd64,armel,armhf,i386
trixie1.8.3-3amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
experimental1.8.4+dfsg-1amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
sid1.8.3-3amd64,arm64,armel,armhf,i386,mips64el,ppc64el,riscv64,s390x
bullseye1.8.3-3amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
bookworm1.8.3-3amd64,arm64,armel,armhf,i386,mips64el,mipsel,ppc64el,s390x
stretch1.7.6+dfsg1-2amd64,arm64,armel,armhf,i386,mips,mips64el,mipsel,ppc64el,s390x
Popcon: 5 users (17 upd.)*
Versions and Archs
License: DFSG free

The Coin-MP optimizer is an open source solver, it is part of the COIN-OR project which is an initiative to spur the development of open-source software for the operations research community.

CoinMP is a C-API library that supports most of the functionality of CLP (Coin LP), CBC (Coin Branch-and-Cut), and CGL (Cut Generation Library) projects.

This package contains the files needed to build applications using libCoinMP.

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