We present completion methods for rewriting modulo a congruence, generalizing previous methods by Peterson and Stickel (1981) and Jouannaud and Kirchner (1986). We formalize our me...
act Completion (Full Version) Guillaume Burel Claude Kirchner August 6, 2007 Deduction Modulo implements Poincar´e’s principle by identifying deduction and computation as diff...
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...
In deduction modulo, a theory is not represented by a set of axioms but by a congruence on propositions modulo which the inference rules of standard deductive systems--such as for ...