Ceci est une ancienne révision du document !


Automatic theorem provers

Zenon

Zenon is an automatic theorem 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

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

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

 
automatic_theorem_provers.1383563863.txt.gz · Dernière modification: Le 04/11/2013 à 12:17 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ó