[DDG13] Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo

Conférence Internationale avec comité de lecture : Logic for Programming Artificial Intelligence and Reasoning (LPAR), December 2013, Vol. 8312, pp.274-290, Series LNCS/ARCoSS, Stellenbosch, South Africa,

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

Mots clés: Tableaux, Deduction Modulo, Rewriting, Automated Theorem Proving, Proof Checking, Zenon, Dedukti

Résumé: 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 lambda-pi-calculus modulo.

Equipe: sys

Collaboration: INRIA , CRI

BibTeX

@inproceedings {
	DDG13,
	title	=	"{Zenon Modulo: When Achilles Outruns the Tortoise using Deduction Modulo}",
	author	=	" D. Delahaye and D. Doligez and F. Gilbert and P. Halmagrand and O. Hermant ",
	booktitle	=	"{Logic for Programming Artificial Intelligence and Reasoning (LPAR)}",
	year	=	2013,
	edition	=	"Springer",
	month	=	"December",
	series	=	"LNCS/ARCoSS",
	volume	=	8312,
	pages	=	"274-290",
	address	=	"Stellenbosch, South Africa",
}