Zenon: an Extensible Automated Theorem Prover Producing Checkable Proofs

Abstract : We present Zenon, an automated theorem prover for first order classical logic (with equality), based on the tableau method. Zenon is intended to be the dedicated prover of the Focal environment, an object-oriented algebraic specification and proof system, which is able to produce OCaml code for execution and Coq code for certification. Zenon can directly generate Coq proofs (proof scripts or proof terms), which can be reinserted in the Coq specifications produced by Focal. Zenon can also be extended, which makes specific (and possibly local) automation possible in Focal.
Type de document :
Communication dans un congrès
LPAR 2007 - 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Oct 2007, Yerevan, Armenia. Springer, 4790, pp.151-165, 2007, Lecture Notes in Computer Science. <10.1007/978-3-540-75560-9_13>


https://hal.inria.fr/inria-00315920
Contributeur : Damien Doligez <>
Soumis le : lundi 1 septembre 2008 - 17:09:46
Dernière modification le : mardi 13 décembre 2016 - 01:05:20
Document(s) archivé(s) le : vendredi 5 octobre 2012 - 12:03:22

Fichier

bonichon-delahaye-doligez-lpar...
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Richard Bonichon, David Delahaye, Damien Doligez. Zenon: an Extensible Automated Theorem Prover Producing Checkable Proofs. LPAR 2007 - 14th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Oct 2007, Yerevan, Armenia. Springer, 4790, pp.151-165, 2007, Lecture Notes in Computer Science. <10.1007/978-3-540-75560-9_13>. <inria-00315920>

Partager

Métriques

Consultations de
la notice

281

Téléchargements du document

120