Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo

Abstract : We propose an extension of the tableau-based first order automated theorem prover Zenon to deduction modulo. The theory of deduction modulo is an extension of predicate calculus, which allows us to rewrite terms as well as propositions, and which is well suited for proof search in axiomatic theories, as it turns axioms into rewrite rules. We also present a heuristic to perform this latter step automatically, and assess our approach by providing some experimental results obtained on the benchmarks provided by the TPTP library, where this heuristic is able to prove difficult problems in set theory in particular. Finally, we describe an additional backend for Zenon that outputs proof certificates for Dedukti, which is a proof checker based on the λΠ-calculus modulo.
Type de document :
Communication dans un congrès
Ken McMillan and Aart Middeldorp and Andrei Voronkov. LPAR - Logic for Programming Artificial Intelligence and Reasoning - 2013, Dec 2013, Stellenbosch, South Africa. Springer, 8312, pp.274-290, 2013, LNCS; Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings. <10.1007/978-3-642-45221-5_20>
Liste complète des métadonnées


https://hal.inria.fr/hal-00909784
Contributeur : Damien Doligez <>
Soumis le : jeudi 26 décembre 2013 - 07:00:04
Dernière modification le : mardi 13 décembre 2016 - 15:42:48
Document(s) archivé(s) le : mercredi 26 mars 2014 - 22:05:17

Fichier

Zenon-modulo-lpar-19.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant. Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo. Ken McMillan and Aart Middeldorp and Andrei Voronkov. LPAR - Logic for Programming Artificial Intelligence and Reasoning - 2013, Dec 2013, Stellenbosch, South Africa. Springer, 8312, pp.274-290, 2013, LNCS; Logic for Programming, Artificial Intelligence, and Reasoning - 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings. <10.1007/978-3-642-45221-5_20>. <hal-00909784>

Partager

Métriques

Consultations de
la notice

776

Téléchargements du document

163