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 
Release  Version  Architectures 
wheezy  2.3.0.12  all 
jessie  2.3.2.21  all 
sid  2.3.2.21  all 
Debtags of package agda: 
role  metapackage 

License: DFSG free

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
MartinLö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.


Altergo
Automatic theorem prover dedicated to program verification

Versions of package altergo 
Release  Version  Architectures 
squeeze  0.912  amd64,armel,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,sparc 
wheezy  0.942  amd64,armel,armhf,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,s390x,sparc 
jessie  0.95.22  amd64,armel,armhf,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
sid  0.95.22  amd64,armel,armhf,hurdi386,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
Debtags of package altergo: 
role  program 
uitoolkit  gtk 
Popcon:
25 users (60 upd.) ^{*}

License: DFSG free

AltErgo 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. AltErgo has
builtin provers for propositional logic, linear arithmetic,
uninterpreted function symbols, associativecommutative function
symbols, polymorphic arrays, userdefined polymorphic record types
and polymorphic enumeration types. It has restricted support for
reasoning over arbitrary userdefined algebraic types, firstorder
quantifiers, and nonlinear arithmetic.
This package contains the prover as a commandline executable
as well as the graphical interface.


Boolector
SMT solver for bitvectors and arrays

Versions of package boolector 
Release  Version  Architectures 
squeeze  1.4.ffc2089.1006081  amd64,armel,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,sparc 
wheezy  1.4.ffc2089.1006081  amd64,armel,armhf,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,s390x,sparc 
jessie  1.5.118.6b56be4.1210131  amd64,armel,armhf,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
sid  1.5.118.6b56be4.1210131  amd64,armel,armhf,hurdi386,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
upstream  1.6.0with.sat.solvers 
Debtags of package boolector: 
role  program 

License: DFSG free

Boolector is an efficient SMT solver for the quantifierfree theory of
bitvectors in combination with the quantifierfree extensional theory of
arrays.


Clasp
conflictdriven nogood learning answer set solver

Versions of package clasp 
Release  Version  Architectures 
wheezy  2.0.62  amd64,armel,armhf,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,s390x,sparc 
jessie  3.0.31  amd64,armel,armhf,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
sid  3.0.31  amd64,armel,armhf,hurdi386,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
Debtags of package clasp: 
field  mathematics 
interface  commandline 
role  program 
Popcon:
25 users (47 upd.) ^{*}

License: DFSG free

clasp is an answer set solver for (extended) normal logic
programs. It combines the highlevel modeling capacities of answer
set programming (ASP) with stateoftheart techniques from the area
of Boolean constraint solving. The primary clasp algorithm relies on
conflictdriven 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 conflictdriven
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 
Release  Version  Architectures 
wheezy  1.0.15  amd64,armel,armhf,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,s390x,sparc 
jessie  1.0.15  amd64,armel,armhf,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
sid  1.0.15  amd64,armel,armhf,hurdi386,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
Debtags of package coala: 
role  program 

License: DFSG free

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.


Coinorcbc
Coinor branchandcut mixed integer programming solver

Versions of package coinorcbc 
Release  Version  Architectures 
jessie  2.8.71  amd64,armel,armhf,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
sid  2.8.71  amd64,armel,armhf,hurdi386,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
upstream  2.8.9 

License: DFSG free

Cbc (Coinor branch and cut) is an opensource mixed integer programming
solver written in C++. It can be used as a callable library or as a
standalone executable.
This package contains cbc executable.


Coq
proof assistant for higherorder logic (toplevel and compiler)

Versions of package coq 
Release  Version  Architectures 
squeeze  8.2.pl2+dfsg1  amd64,armel,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,sparc 
wheezy  8.3.pl4+dfsg2  amd64,armel,armhf,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,s390x,sparc 
jessie  8.4pl3dfsg1  amd64,armel,armhf,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
sid  8.4pl3dfsg1  amd64,armel,armhf,hurdi386,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
Debtags of package coq: 
devel  compiler 
field  mathematics 
interface  textmode, commandline 
role  program 
scope  utility 
uitoolkit  ncurses 
Popcon:
115 users (65 upd.) ^{*}

License: DFSG free

Coq is a proof assistant for higherorder 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.


Cvc3
Automatic theorem prover for SMT problems

Versions of package cvc3 
Release  Version  Architectures 
squeeze  2.213  amd64,armel,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,sparc 
wheezy  2.4.14  amd64,armel,armhf,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,s390x,sparc 
jessie  2.4.14  amd64,armel,armhf,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
sid  2.4.14  amd64,armel,armhf,hurdi386,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
Debtags of package cvc3: 
interface  commandline 
role  program 

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 firstorder formulas in a large number of builtin
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 firstorder logic with polymorphic types
and has a wide variety of features including:
 several builtin 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 textbased 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:
cvc3el


Depqbf
solver for quantified boolean formulae

Versions of package depqbf 
Release  Version  Architectures 
wheezy  0.11  amd64,armel,armhf,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,s390x,sparc 
jessie  3.01  amd64,armel,armhf,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
sid  3.011  armhf,mips,mipsel,sparc 
sid  3.021  amd64,armel,hurdi386,i386,kfreebsdamd64,kfreebsdi386,powerpc,s390x 

License: DFSG free

DepQBF is a searchbased solver for quantified boolean formulae (QBF)
in prenex conjunctive normal form. It is based on the DPLL algorithm
for QBF, called QDPLL, with conflictdriven clause and solutiondriven
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 socalled "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 
Release  Version  Architectures 
wheezy  3.0.43  amd64,armel,armhf,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,s390x,sparc 
jessie  4.3.01  amd64,armel,armhf,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
sid  4.3.01  amd64,armel,armhf,hurdi386,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
Debtags of package gringo: 
role  program 
Popcon:
26 users (16 upd.) ^{*}

License: DFSG free

Current answer set solvers work on variablefree programs. Hence, a
grounder is needed that, given an input program with firstorder
variables, computes an equivalent ground (variablefree) program.
This package contains the following tools:
 gringo: creates lparsecompatible variablefree 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 reproducing
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.


Hollight

Versions of package hollight 
Release  Version  Architectures 
wheezy  201206021  amd64,armel,armhf,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,s390x,sparc 
jessie  201310261  amd64,armel,armhf,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
sid  201310261  amd64,armel,armhf,hurdi386,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
Popcon:
27 users (12 upd.) ^{*}

License: DFSG free

HOL Light is an interactive theorem prover for HigherOrder Logic
with a very simple logical core running in an OCaml toplevel. HOL
Light is famous for the verification of floatingpoint
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

Versions of package hol88 
Release  Version  Architectures 
squeeze  2.02.1994031613.1  amd64,armel,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,sparc 
wheezy  2.02.1994031615  amd64,armel,armhf,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,s390x,sparc 
jessie  2.02.1994031619  amd64,armel,armhf,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
sid  2.02.1994031619  amd64,armel,armhf,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
Debtags of package hol88: 
uitoolkit  ncurses 

License: DFSG free

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


Lbt
converts from LTL formulas to Büchi automata

Versions of package lbt 
Release  Version  Architectures 
squeeze  1.2.24  amd64,armel,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,sparc 
wheezy  1.2.25  amd64,armel,armhf,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,s390x,sparc 
jessie  1.2.25  amd64,armel,armhf,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
sid  1.2.25  amd64,armel,armhf,hurdi386,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
Debtags of package lbt: 
field  mathematics 
interface  commandline 
role  program 
scope  utility 
use  converting 

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 firstorder statements

Versions of package mace2 
Release  Version  Architectures 
squeeze  3.3f1  amd64,armel,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,sparc 
wheezy  3.3f1.1  amd64,armel,armhf,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,s390x,sparc 
jessie  3.3f1.1  amd64,armel,armhf,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
sid  3.3f1.1  amd64,armel,armhf,hurdi386,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
Debtags of package mace2: 
role  program 
use  searching 

License: DFSG free

MACE is a program that searches for finite models of firstorder 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 firstorder 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 
Release  Version  Architectures 
squeeze  1.3.52  amd64,armel,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,sparc 
wheezy  1.3.54  amd64,armel,armhf,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,s390x,sparc 
jessie  1.3.54  amd64,armel,armhf,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
sid  1.3.54  amd64,armel,armhf,hurdi386,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
Debtags of package maria: 
devel  testingqa 
field  mathematics 
interface  textmode 
role  program 
scope  utility 
uitoolkit  ncurses 

License: DFSG free

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 highlevel
programming languages, thanks to its rich data type system and
powerful algebraic operations.


Matita
interactive theorem prover

Versions of package matita 
Release  Version  Architectures 
squeeze  0.5.82  amd64,armel,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,sparc 
wheezy  0.99.11  amd64,armel,armhf,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,s390x,sparc 
jessie  0.99.13  amd64,armel,armhf,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
sid  0.99.13  amd64,armel,armhf,hurdi386,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
Debtags of package matita: 
field  mathematics 
interface  x11, commandline 
role  program 
uitoolkit  gtk 
use  checking 
x11  application 
Popcon:
27 users (13 upd.) ^{*}

License: DFSG free

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


Maude
highperformance logical framework

Versions of package maude 
Release  Version  Architectures 
wheezy  2.62  amd64,armel,armhf,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,s390x,sparc 
sid  2.64  amd64,armel,armhf,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
Debtags of package maude: 
uitoolkit  ncurses 

License: DFSG free

Maude is a highperformance 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 objectoriented
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.


Minisat+
solver for pseudoBoolean constraints

Versions of package minisat+ 
Release  Version  Architectures 
wheezy  1.02  amd64,armel,armhf,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,s390x,sparc 
jessie  1.02  amd64,armel,armhf,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
sid  1.02  amd64,armel,armhf,hurdi386,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
Debtags of package minisat+: 
field  mathematics 
role  program 

License: DFSG free

MinSat+ is a solver for PseudoBoolean Optimization (AKA 01
integer programming) that is based on the MiniSat SATsolver. 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. PseudoBoolean 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 
Release  Version  Architectures 
squeeze  1.4131  amd64,armel,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,sparc 
wheezy  1.4133  amd64,armel,armhf,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,s390x,sparc 
jessie  1.4133  amd64,armel,armhf,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
sid  1.4133  amd64,armel,armhf,hurdi386,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
Debtags of package mona: 
field  mathematics 
role  program 
scope  utility 

License: DFSG free

MONA is a tool that translates formulas in the logics WS1S or WS2S
into finitestate 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 counterexample.
Documentation is available from the MONA website http://www.brics.dk/mona/.


Otter
resolutionstyle theorem prover

Versions of package otter 
Release  Version  Architectures 
squeeze  3.3f1  amd64,armel,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,sparc 
wheezy  3.3f1.1  amd64,armel,armhf,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,s390x,sparc 
jessie  3.3f1.1  amd64,armel,armhf,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
sid  3.3f1.1  amd64,armel,armhf,hurdi386,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 

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,
KnuthBendix 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

Versions of package picosat 
Release  Version  Architectures 
squeeze  9134  amd64,armel,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,sparc 
wheezy  9364  amd64,armel,armhf,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,s390x,sparc 
jessie  9541  amd64,armel,armhf,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
sid  9541  amd64,armel,armhf,hurdi386,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
upstream  957 
Debtags of package picosat: 
field  mathematics 
role  program 

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 
Release  Version  Architectures 
squeeze  3.74  all 
wheezy  4.2~pre1206052  all 
jessie  4.3~pre1305101.1  all 
sid  4.3~pre1305101.1  all 
upstream  4.3~pre131011 
Debtags of package proofgeneral: 
field  mathematics 
interface  x11, textmode 
role  plugin 
suite  emacs 
use  editing 
Popcon:
44 users (25 upd.) ^{*}

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


Prover9
theorem prover and countermodel generator

Versions of package prover9 
Release  Version  Architectures 
squeeze  0.0.200902a2  amd64,armel,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,sparc 
wheezy  0.0.200902a2.1  amd64,armel,armhf,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,s390x,sparc 
jessie  0.0.200911a2  amd64,armel,armhf,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
sid  0.0.200911a2  amd64,armel,armhf,hurdi386,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
Popcon:
28 users (13 upd.) ^{*}

License: DFSG free

This package provides the Prover9 resolution/paramodulation theorem
prover and the Mace4 countermodel generator.
Prover9 is an automated theorem prover for firstorder 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 firstorder
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

Versions of package sat4j 
Release  Version  Architectures 
squeeze  2.2.03  all 
wheezy  2.3.11  all 
jessie  2.3.21  all 
sid  2.3.21  all 
upstream  2.3.3 
Debtags of package sat4j: 
field  mathematics 
role  sharedlib, program 
Popcon:
2378 users (1183 upd.) ^{*}

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 firstorder logic with equality

Versions of package spass 
Release  Version  Architectures 
squeeze  3.72  amd64,armel,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,sparc 
wheezy  3.73  amd64,armel,armhf,i386,ia64,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390,s390x,sparc 
jessie  3.73  amd64,armel,armhf,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
sid  3.73  amd64,armel,armhf,hurdi386,i386,kfreebsdamd64,kfreebsdi386,mips,mipsel,powerpc,s390x,sparc 
Debtags of package spass: 
field  mathematics 

License: DFSG free

SPASS is a saturationbased automated theorem prover for firstorder 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 betarule of analytic tableaux and the case
analysis employed in the DavisPutnam 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.mpisb.mpg.de/.


