Ceci est une ancienne révision du document !

Automatic theorem provers


Zenon is an automatic theorem prover that handles first-order logic with equality. Its most important feature is that it outputs the proofs of the theorems, in Coq-checkable form.


MetiTarski is an automatic theorem prover based on a combination of resolution and a decision procedure for the theory of real closed fields. It is designed to prove theorems involving real-valued special functions such as log, exp, sin, cos and sqrt. In particular, it is designed to prove universally quantified inequalities involving such functions. This problem is undecidable, so MetiTarski is necessarily incomplete. Nevertheless, MetiTarski is remarkably powerful.

E Theorem Prover

E is a theorem prover for full first-order logic with equality. It accepts a problem specification, typically consisting of a number of first-order clauses or formulas, and a conjecture, again either in clausal or full first-order form. The system will then try to find a formal proof for the conjecture, assuming the axioms.

If a proof is found, the system can provide a detailed list of proof steps that can be individually verified. If the conjecture is existential (i.e. it’s of the form “there exists an X with property P”), the latest versions can also provide possible answers (values for X).


SPASS is an automated theorem prover for first-order logic with equality.


SPIKE is an automated theorem prover using (first-order) formula-based Noetherian induction. Spike can be called from the Coq proof assistant using a tactic that automatically performs lazy and mutual induction. We provide a zip file with the Coq scripts using this tactic. Spike proofs can be checked with Coq.


Psyche is a modular platform for automated or interactive theorem proving, programmed in OCaml and built on an architecture (similar to LCF) where a small kernel interacts with plugins and decision procedures:

  • The kernel is based on a proof-search engine à la Prolog, offering an API to perform incremental and goal-directed constructions of proof-trees in (a standard but carefully chosen) Sequent Calculus, which can be seen as a tableau method.
  • Psyche can produce proof objects.
  • Plugins can be programmed to drive the kernel, using its API, through the search space towards an answer provable or not provable; soundness of the answer only relies on the kernel via the use of a private type for answers (similar to LCF’s theorem type).
  • Plugins can be interactive.
  • Psyche offers a memoisation feature to help programming efficient plugins.
  • The kernel is parameterised by a procedure deciding the consistency of collections of literals with respect to a background theory, just as in SAT-modulo-theories (SMT) solvers.
automatic_theorem_provers.1422030301.txt.gz · Dernière modification: Le 23/01/2015 à 17:25 par david_mentre     Haut de page
Recent changes RSS feed Powered by PHP Valid XHTML 1.0 Valid CSS Driven by DokuWiki Design by Chirripó