Theorem proving modulo (Q1431339): Difference between revisions

The authors argue that theorem proving can be divided into a computation part and a deduction part. Deduction modulo is a method to remove the computational arguments from proofs. A proof search method is presented based on extended narrowing and resolution which is sound and complete with respect to the sequent calculus modulo, for a large class of congruences.