Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps - Archive ouverte HAL Access content directly
Conference Papers Year : 2013

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

(1) , (2) , (3) , (1) , (4)
1
2
3
4

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.
Fichier principal
Vignette du fichier
zenon-modulo-iwil-2013.pdf (115.71 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-00909688 , version 1 (26-11-2013)

Identifiers

  • HAL Id : hal-00909688 , version 1

Cite

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. IWIL - 10th International Workshop on the Implementation of Logics - 2013, Dec 2013, Stellenbosch, South Africa. ⟨hal-00909688⟩
396 View
91 Download

Share

Gmail Facebook Twitter LinkedIn More