Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps

Abstract : We present the certifying part of the Zenon Modulo automated theorem prover, which is an extension of the Zenon tableau-based first order automated theorem prover 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. In addition, deduction modulo allows Zenon Modulo to compress proofs by making computations implicit in proofs. To certify these proofs, we use Dedukti, an external proof checker for the λΠ-calculus modulo, which can deal natively with proofs in deduction modulo. To assess our approach, we rely on some experimental results obtained on the benchmarks provided by the TPTP library.
Type de document :
Communication dans un congrès
Stephan Schulz and Geoff Sutcliffe and Boris Konev. IWIL - 10th International Workshop on the Implementation of Logics - 2013, Dec 2013, Stellenbosch, South Africa. EasyChair, 2013
Liste complète des métadonnées


https://hal.inria.fr/hal-00909688
Contributeur : Damien Doligez <>
Soumis le : mardi 26 novembre 2013 - 16:27:26
Dernière modification le : jeudi 29 septembre 2016 - 01:24:18
Document(s) archivé(s) le : jeudi 27 février 2014 - 10:40:24

Fichier

zenon-modulo-iwil-2013.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00909688, version 1

Collections

Citation

David Delahaye, Damien Doligez, Frédéric Gilbert, Pierre Halmagrand, Olivier Hermant. Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps. Stephan Schulz and Geoff Sutcliffe and Boris Konev. IWIL - 10th International Workshop on the Implementation of Logics - 2013, Dec 2013, Stellenbosch, South Africa. EasyChair, 2013. <hal-00909688>

Partager

Métriques

Consultations de
la notice

416

Téléchargements du document

124