91c0a04f8a6d3c1121460346e0e12cf40c4e1faaJonathan von SchroederSource: satallax
91c0a04f8a6d3c1121460346e0e12cf40c4e1faaJonathan von SchroederMaintainer: Jonathan von Schroeder <jonathan.von_schroeder@dfki.de>
343b5264cd1b9da8cb5a8ca63b17d29cb77d33fcJonathan von SchroederBuild-Depends: debhelper (>= 7.4.15), autotools-dev, help2man, zlib1g-dev, ocaml
91c0a04f8a6d3c1121460346e0e12cf40c4e1faaJonathan von SchroederStandards-Version: 3.9.3
91c0a04f8a6d3c1121460346e0e12cf40c4e1faaJonathan von SchroederHomepage: http://www.ps.uni-saarland.de/~cebrown/satallax/
91c0a04f8a6d3c1121460346e0e12cf40c4e1faaJonathan von SchroederPackage: satallax
91c0a04f8a6d3c1121460346e0e12cf40c4e1faaJonathan von SchroederArchitecture: amd64 i386
91c0a04f8a6d3c1121460346e0e12cf40c4e1faaJonathan von SchroederDepends: ${shlibs:Depends}, ${misc:Depends}, zlib1g-dev, ocaml, eprover
91c0a04f8a6d3c1121460346e0e12cf40c4e1faaJonathan von SchroederDescription: Automated theorem prover for higher-order logic
91c0a04f8a6d3c1121460346e0e12cf40c4e1faaJonathan von Schroeder Satallax is an automated theorem prover for higher-order logic.
91c0a04f8a6d3c1121460346e0e12cf40c4e1faaJonathan von Schroeder The particular form of higher-order logic supported by Satallax is
91c0a04f8a6d3c1121460346e0e12cf40c4e1faaJonathan von Schroeder Church's simple type theory with extensionality and choice operators.
91c0a04f8a6d3c1121460346e0e12cf40c4e1faaJonathan von Schroeder The SAT solver MiniSat is responsible for much of the search for a proof.
91c0a04f8a6d3c1121460346e0e12cf40c4e1faaJonathan von Schroeder Satallax generates propositional clauses corresponding to rules of a complete
91c0a04f8a6d3c1121460346e0e12cf40c4e1faaJonathan von Schroeder tableau calculus and calls MiniSat periodically to test satisfiability of
91c0a04f8a6d3c1121460346e0e12cf40c4e1faaJonathan von Schroeder these clauses. Satallax is implemented in Objective Caml.