Source: satallax
Priority: extra
Section: misc
Maintainer: Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>
Build-Depends: debhelper (>= 7.4.15), autotools-dev, help2man, zlib1g-dev, ocaml
Standards-Version: 3.9.3
Package: satallax
Architecture: amd64 i386
Depends: ${shlibs:Depends}, ${misc:Depends}, zlib1g-dev, ocaml, eprover
Description: Automated theorem prover for higher-order logic
Satallax is an automated theorem prover for higher-order logic.
The particular form of higher-order logic supported by Satallax is
Church's simple type theory with extensionality and choice operators.
The SAT solver MiniSat is responsible for much of the search for a proof.
Satallax generates propositional clauses corresponding to rules of a complete
tableau calculus and calls MiniSat periodically to test satisfiability of
these clauses. Satallax is implemented in Objective Caml.