×

zbMATH — the first resource for mathematics

Theorem proving modulo. (English) Zbl 1049.03011
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.

MSC:
03B35 Mechanization of proofs and logical operations
03F05 Cut-elimination and normal-form theorems
PDF BibTeX XML Cite
Full Text: DOI