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.

The list to the right includes various software projects which are of some interest to the Debian Science Project. Currently, only a few of them are available as Debian packages. It is our goal, however, to include all software in Debian Science which can sensibly add to a high quality Debian Pure Blend.

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
dependently typed functional programming language
Versions of package agda
ReleaseVersionArchitectures
wheezy2.3.0.1-2all
sid2.3.2.2-1all
jessie2.4.0.2-2all
sid2.4.0.2-2all
upstream2.4.2
Debtags of package agda:
rolemetapackage
Popcon: 0 users (0 upd.)*
Newer upstream!
License: DFSG free
Git

Agda is a dependently typed functional programming language: It has inductive families, which are like Haskell's GADTs, but they can be indexed by values and not just types. It also has parameterised modules, mixfix operators, Unicode characters, and an interactive Emacs interface (the type checker can assist in the development of your code).

Agda is also a proof assistant: It is an interactive system for writing and checking proofs. Agda is based on intuitionistic type theory, a foundational system for constructive mathematics developed by the Swedish logician Per Martin-Löf. It has many similarities with other proof assistants based on dependent types, such as Coq, Epigram and NuPRL.

This is a meta package which provides Agda's emacs mode, executable, standard library and its documentation.

Alt-ergo
Automatic theorem prover dedicated to program verification
Versions of package alt-ergo
ReleaseVersionArchitectures
squeeze0.91-2amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy0.94-2amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie0.95.2-3amd64,arm64,armel,armhf,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x
sid0.95.2-3amd64,arm64,armel,armhf,hurd-i386,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x,sparc
Debtags of package alt-ergo:
roleprogram
uitoolkitgtk
Popcon: 15 users (11 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 as well as the graphical interface.

Boolector
SMT solver for bit-vectors and arrays
Maintainer: Michael Tautschnig
Versions of package boolector
ReleaseVersionArchitectures
squeeze1.4.ffc2089.100608-1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy1.4.ffc2089.100608-1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie1.5.118.6b56be4.121013-1amd64,arm64,armel,armhf,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x
sid1.5.118.6b56be4.121013-1amd64,arm64,armel,armhf,hurd-i386,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x,sparc
upstream1.6.0-with.sat.solvers
Debtags of package boolector:
roleprogram
Popcon: 0 users (2 upd.)*
Newer upstream!
License: DFSG free

Boolector is an efficient SMT solver for the quantifier-free theory of bit-vectors in combination with the quantifier-free extensional theory of arrays.

Clasp
conflict-driven nogood learning answer set solver
Versions of package clasp
ReleaseVersionArchitectures
wheezy2.0.6-2amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie3.1.0-1amd64,arm64,armel,armhf,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x
sid3.1.0-1amd64,arm64,armel,armhf,hurd-i386,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x,sparc
Debtags of package clasp:
roleprogram
Popcon: 32 users (15 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).

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

The coala tool translates an action language into a logic program under the answer set semantics. After being grounded by lparse or gringo, the logic program can be solved by an answer set solver such as clasp. At the moment coala is able to translate the action language AL, B, C, a subset of C+ and the action language CTAID. The type of input language can be specified with a command line option.

Coinor-cbc
Coin-or branch-and-cut mixed integer programming solver
Versions of package coinor-cbc
ReleaseVersionArchitectures
jessie2.8.12-1amd64,arm64,armel,armhf,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x
sid2.8.12-1amd64,arm64,armel,armhf,hurd-i386,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x,sparc
Popcon: 7 users (6 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.

Coq
proof assistant for higher-order logic (toplevel and compiler)
Versions of package coq
ReleaseVersionArchitectures
squeeze8.2.pl2+dfsg-1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy8.3.pl4+dfsg-2amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie8.4pl4dfsg-1amd64,arm64,armel,armhf,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x
sid8.4pl4dfsg-1amd64,arm64,armel,armhf,hurd-i386,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x,sparc
Debtags of package coq:
develcompiler
fieldmathematics
interfacetext-mode, commandline
roleprogram
scopeutility
uitoolkitncurses
Popcon: 156 users (40 upd.)*
Versions and Archs
License: DFSG free
Git

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

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

A graphical interface for Coq is provided in the coqide package. Coq can also be used with ProofGeneral, which allows proofs to be edited using emacs and xemacs. This requires the proofgeneral package to be installed.

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

CVC3 is an automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination.

CVC3 is the last offspring of a series of popular SMT provers, which originated at Stanford University with the SVC system. In particular, it builds on the code base of CVC Lite, its most recent predecessor. Its high level design follows that of the Sammy prover.

CVC3 works with a version of first-order logic with polymorphic types and has a wide variety of features including:

  • several built-in base theories: rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bit vectors, and equality over uninterpreted function symbols;
  • support for quantifiers;
  • an interactive text-based interface;
  • rich C, C++, and Java APIs for embedding in other systems;
  • proof and model generation abilities;
  • predicate subtyping;
  • essentially no limit on its use for research or commercial purposes (see license).

This package contains the CVC3 command line program.

The package is enhanced by the following packages: cvc3-el
Depqbf
solver for quantified boolean formulae
Versions of package depqbf
ReleaseVersionArchitectures
wheezy0.1-1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie3.04-1amd64,arm64,armel,armhf,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x
sid3.04-1amd64,arm64,armel,armhf,hurd-i386,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x,sparc
Popcon: 1 users (11 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.

Gringo
grounding tools for (disjunctive) logic programs
Versions of package gringo
ReleaseVersionArchitectures
wheezy3.0.4-3amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie4.4.0-1amd64,arm64,armel,armhf,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x
sid4.4.0-1amd64,arm64,armel,armhf,hurd-i386,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x,sparc
Debtags of package gringo:
roleprogram
Popcon: 29 users (15 upd.)*
Versions and Archs
License: DFSG free
Git

Current answer set solvers work on variable-free programs. Hence, a grounder is needed that, given an input program with first-order variables, computes an equivalent ground (variable-free) program.

This package contains the following tools:

  • gringo: creates lparse-compatible variable-free programs.
  • clingo: stands for clasp on gringo and combines both systems in a monolithic way. Its input language is that of gringo and its output corresponds to that of clasp.
  • iclingo: an incremental answer set programming system, which is based on the idea that the grounder as well as the solver are implemented in a stateful way. Thus, both keep their previous states while increasing an incremental parameter. As regards grounding, at each incremental step, the goal is to produce only ground rules stemming from the current program slice, without re-producing previous ground rules. The ground program slices are then gradually passed to the solver that accumulates ground rules and computes answer sets for them.
  • oclingo: a system for reactive answer set programming, extending gringo and clasp for handling external modules provided at runtime by a controller.
Hol-light
HOL Light theorem prover
Versions of package hol-light
ReleaseVersionArchitectures
wheezy20120602-1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie20131026-1amd64,arm64,armel,armhf,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x
sid20131026-1amd64,arm64,armel,armhf,hurd-i386,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x,sparc
Popcon: 24 users (6 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 aims at the formalization of Tom Hales' proof of the Kepler conjecture.

Hol88
Higher Order Logic, system image
Maintainer: Camm Maguire
Versions of package hol88
ReleaseVersionArchitectures
squeeze2.02.19940316-13.1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy2.02.19940316-15amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie2.02.19940316-27amd64,arm64,armel,armhf,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x
sid2.02.19940316-27mips
sid2.02.19940316-28amd64,arm64,armel,armhf,i386,kfreebsd-amd64,kfreebsd-i386,mipsel,powerpc,ppc64el,s390x,sparc
Debtags of package hol88:
uitoolkitncurses
Popcon: 4 users (5 upd.)*
Versions and Archs
License: DFSG free

The HOL System is an environment for interactive theorem proving in a higher-order logic. Its most outstanding feature is its high degree of programmability through the meta-language ML. The system has a wide variety of uses from formalizing pure mathematics to verification of industrial hardware. Academic and industrial sites world-wide are using HOL.

Lbt
converts from LTL formulas to Büchi automata
Versions of package lbt
ReleaseVersionArchitectures
squeeze1.2.2-4amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy1.2.2-5amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie1.2.2-5amd64,arm64,armel,armhf,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x
sid1.2.2-5amd64,arm64,armel,armhf,hurd-i386,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x,sparc
Debtags of package lbt:
fieldmathematics
interfacecommandline
roleprogram
scopeutility
useconverting
Popcon: 3 users (2 upd.)*
Versions and Archs
License: DFSG free

This software converts a linear temporal logic (ltl) formula to a generalised Büchi automaton. The resulting automaton may be used, for instance, in model checking, where it represents a property to be verified from a model (e.g. a Petri net).

Mace2
program that searches for finite models of first-order statements
Versions of package mace2
ReleaseVersionArchitectures
squeeze3.3f-1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy3.3f-1.1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie3.3f-1.1amd64,arm64,armel,armhf,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x
sid3.3f-1.1amd64,arm64,armel,armhf,hurd-i386,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x,sparc
Debtags of package mace2:
roleprogram
usesearching
Popcon: 2 users (2 upd.)*
Versions and Archs
License: DFSG free

MACE is a program that searches for finite models of first-order and equational statements developed at Argonne National Laboratory.

This package includes ANLDP, which calls the propositional decision procedure at the core of MACE directly.

MACE serves as a complementary companion to OTTER, which searches for refutations of the same class of statement. In particular, if you have a first-order conjecture, OTTER will search for a proof, and MACE will search for a counterexample from the same input file.

Maria
reachability analyzer for Algebraic System Nets
Versions of package maria
ReleaseVersionArchitectures
squeeze1.3.5-2amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy1.3.5-4amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie1.3.5-4amd64,arm64,armel,armhf,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x
sid1.3.5-4amd64,arm64,armel,armhf,hurd-i386,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x,sparc
Debtags of package maria:
develtesting-qa
fieldmathematics
interfacetext-mode
roleprogram
scopeutility
uitoolkitncurses
Popcon: 10 users (1 upd.)*
Versions and Archs
License: DFSG free
Git

Maria is a powerful tool designed to aid engineers in modelling and solving concurrency related problems in parallel and distributed computing systems.

Maria finds deadlocks and violations against safety or liveness requirements by exploring all states that can be reached from the initial state of a system. The tool manages tens or hundreds of millions of reachable states and enabled actions.

The expressive power of Maria's formalism is close to high-level programming languages, thanks to its rich data type system and powerful algebraic operations.

Matita
interactive theorem prover
Versions of package matita
ReleaseVersionArchitectures
squeeze0.5.8-2amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy0.99.1-1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie0.99.1-3amd64,arm64,armel,armhf,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x
sid0.99.1-3amd64,arm64,armel,armhf,hurd-i386,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x,sparc
Debtags of package matita:
fieldmathematics
interfacex11, commandline
roleprogram
uitoolkitgtk
usechecking
x11application
Popcon: 25 users (4 upd.)*
Versions and Archs
License: DFSG free
Git

Matita is a graphical interactive theorem prover based on the Calculus of (Co)Inductive Constructions.

Screenshots of package matita
Maude
high-performance logical framework
Versions of package maude
ReleaseVersionArchitectures
wheezy2.6-2amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie2.6-6amd64,arm64,armel,armhf,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x
sid2.6-6amd64,arm64,armel,armhf,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x,sparc
Debtags of package maude:
uitoolkitncurses
Popcon: 2 users (13 upd.)*
Versions and Archs
License: DFSG free
Svn

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
wheezy1.0-2amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie1.0-2amd64,arm64,armel,armhf,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x
sid1.0-2amd64,arm64,armel,armhf,hurd-i386,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x,sparc
Debtags of package minisat+:
fieldmathematics
roleprogram
Popcon: 3 users (3 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 prover based on automata
Versions of package mona
ReleaseVersionArchitectures
squeeze1.4-13-1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy1.4-13-3amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie1.4-15-1amd64,arm64,armel,armhf,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x
sid1.4-15-1amd64,arm64,armel,armhf,hurd-i386,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x,sparc
Debtags of package mona:
fieldmathematics
roleprogram
scopeutility
Popcon: 9 users (0 upd.)*
Versions and Archs
License: DFSG free
Git

MONA is a tool that translates formulas in the logics WS1S or WS2S into finite-state automata represented by BDDs. The formulas may express search patterns, temporal properties of reactive systems, parse tree constraints, etc. MONA also analyses the automaton resulting from the compilation, and determines whether the formula is valid and, if the formula is not valid, generates a counter-example.

Documentation is available from the MONA website http://www.brics.dk/mona/.

Otter
resolution-style theorem prover
Versions of package otter
ReleaseVersionArchitectures
squeeze3.3f-1amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy3.3f-1.1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie3.3f-1.1amd64,arm64,armel,armhf,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x
sid3.3f-1.1amd64,arm64,armel,armhf,hurd-i386,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x,sparc
Popcon: 1 users (2 upd.)*
Versions and Archs
License: DFSG free

OTTER is an automated theorem prover for equational logic developed at Argonne National Laboratory.

OTTER's inference rules are based on resolution and paramodulation, and it includes facilities for term rewriting, term orderings, Knuth-Bendix completion, weighting, and strategies for directing and restricting searches for proofs. OTTER can also be used as a symbolic calculator and has an embedded equational programming system.

Picosat
SAT solver with proof and core support
Maintainer: Michael Tautschnig
Versions of package picosat
ReleaseVersionArchitectures
squeeze913-4amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy936-4amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie959-1amd64,arm64,armel,armhf,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x
sid959-1amd64,arm64,armel,armhf,hurd-i386,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x,sparc
upstream960
Debtags of package picosat:
fieldmathematics
roleprogram
Popcon: 3 users (2 upd.)*
Newer upstream!
License: DFSG free

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.

Proofgeneral
generic frontend for proof assistants
Versions of package proofgeneral
ReleaseVersionArchitectures
squeeze3.7-4all
wheezy4.2~pre120605-2all
jessie4.3~pre131011-0.1all
sid4.3~pre131011-0.1all
Debtags of package proofgeneral:
fieldmathematics
interfacex11, text-mode
roleplugin
suiteemacs
useediting
Popcon: 91 users (13 upd.)*
Versions and Archs
License: DFSG free

Proof General is a major mode to turn Emacs into an interactive proof assistant to write formal mathematical proofs using a variety of theorem provers.

This package provides Proof General support for Coq. (There is no other proof assistant that one could sensibly support.)

Screenshots of package proofgeneral
Prover9
theorem prover and countermodel generator
Versions of package prover9
ReleaseVersionArchitectures
squeeze0.0.200902a-2amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy0.0.200902a-2.1amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie0.0.200911a-2.1amd64,arm64,armel,armhf,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x
sid0.0.200911a-2.1amd64,arm64,armel,armhf,hurd-i386,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x,sparc
Popcon: 24 users (47 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
Efficient library of SAT solvers in Java
Maintainer: Michael Tautschnig
Versions of package sat4j
ReleaseVersionArchitectures
squeeze2.2.0-3all
wheezy2.3.1-1all
jessie2.3.3-1all
sid2.3.3-1all
Debtags of package sat4j:
fieldmathematics
roleshared-lib, program
Popcon: 1916 users (1310 upd.)*
Versions and Archs
License: DFSG free

The aim of the SAT4J library is to provide an efficient library of SAT solvers in Java. Compared to the OpenSAT project, the SAT4J library targets first users of SAT "black boxes", willing to embed SAT technologies into their application without worrying about the details. The SAT4J project also tries to provide a basis of work for SAT researchers.

Spass
An automated theorem prover for first-order logic with equality
Maintainer: Roland Stigge
Versions of package spass
ReleaseVersionArchitectures
squeeze3.7-2amd64,armel,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,sparc
wheezy3.7-3amd64,armel,armhf,i386,ia64,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,s390,s390x,sparc
jessie3.7-3amd64,arm64,armel,armhf,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x
sid3.7-3amd64,arm64,armel,armhf,hurd-i386,i386,kfreebsd-amd64,kfreebsd-i386,mips,mipsel,powerpc,ppc64el,s390x,sparc
Debtags of package spass:
fieldmathematics
Popcon: 2 users (1 upd.)*
Versions and Archs
License: DFSG free

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.

For more information, additional and partly huge example collections, consider the project homepage at http://spass.mpi-sb.mpg.de/.

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