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.

• Type: Conference
• Year: 2004
• Where: CADE
• Authors: Richard Bonichon
• Keywords: Automated Reasoning, CADE 2004, Deduction Modulo, Sequent Calculus Modulo, Theorem Proving Modulo