TaMeD: A Tableau Method for Deduction Modulo

11 years 4 months ago
TaMeD: A Tableau Method for Deduction Modulo
Deduction modulo is a theoretical framework for reasoning modulo a congruence on propositions. Computational steps are thus removed from proofs, thus allowing a clean separatation of computational and deductive steps. A sequent calculus modulo has been defined in (Dowek et al., 2003) as well as a resolution-based proof search method, in which the congruences are handled through rewrite rules on terms and atomic propositions. This article defines an automated proof search method for theorem proving modulo (TaMeD ) based upon free-variable tableaus for classical logic . Syntactic proofs for the soundness and completeness of the method are given with respect to provability in the sequent calculus modulo. The proofs follow a pattern similar to those of ENAR so that comparisons between some characteristics of the two methods can be drawn. Finally, some applications of deduction modulo as well as hints at further or ongoing research in this field are briefly presented.
Richard Bonichon
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2004
Where CADE
Authors Richard Bonichon
Comments (0)