Anciennes révisions Liens vers cette page Afficher le texte source
 Index Derniers changements

Ceci est une ancienne révision du document !

Table des matières

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