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

Conférence Internationale avec comité de lecture : International Workshop on the Implementation of Logics, December 2013, pp.-,

Auteurs: D. Delahaye , D. Doligez , F. Gilbert , P. Halmagrand , O. Hermant

Mots clés: Tableaux, Deduction Modulo, Automated Theorem Proving, Proof Compression, Proof Verification, Zenon, Dedukti

Résumé: 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 lambda-Pi-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.

Equipe: sys

Collaboration: INRIA , CRI

BibTeX

@inproceedings {
	DDG13a,
	title	=	"{Proof Certification in Zenon Modulo: When Achilles Uses Deduction Modulo to Outrun the Tortoise with Shorter Steps}",
	author	=	" D. Delahaye and D. Doligez and F. Gilbert and P. Halmagrand and O. Hermant ",
	booktitle	=	"{International Workshop on the Implementation of Logics}",
	year	=	2013,
	month	=	"December",
	pages	=	"-",
}