TaMeD: A Tableau Method For Deduction Modulo

Abstract

Deduction modulo is a formalism introduced to separate cleanly computations and deductions by reasoning modulo a congruence on propositions. A sequent calculus modulo has been defined by Dowek, Hardin and Kirchner as well as a resolution-based proof search method called Extended Narrowing And Resolution (ENAR), in which the congruences are handled through rewrite rules on terms and atomic propositions. We define a tableau-based proof search method, called Tableau Method for Deduction modulo (TaMeD), for theorem proving modulo. We then give a syntactic proof of the completeness of the method with respect to provability in the sequent calculus modulo. Moreover, we follow in our proofs the same steps as the ENAR method in such a way that it allows to try and compare the characteristics of both methods.