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.
Complete list of metadatas

Cited literature [7 references]  Display  Hide  Download

https://hal.inria.fr/hal-00909688
Contributor : Damien Doligez <>
Submitted on : Tuesday, November 26, 2013 - 4:27:26 PM
Last modification on : Saturday, February 9, 2019 - 1:24:17 AM
Long-term archiving on : Thursday, February 27, 2014 - 10:40:24 AM

File

zenon-modulo-iwil-2013.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00909688, version 1

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

Share

Metrics

Record views

640

Files downloads

167