Proof Transformations for Equational Theories

Tobias Nipkow

This paper contrasts two kinds of proof systems for equational theories: the standard ones obtained by combining the axioms with the laws of equational logic, and alternative systems designed to yield decision procedures for equational problems.

Although new matching algorithms for (among other theories) associativity, associativity + commutativity, and associativity + commutativity + identity are presented, the emphasis is not so much on individual theories but on the general method of proof transformation as a tool for showing the equivalence of different proof systems.

After studying proof translations defined by rewriting systems, equivalence tests based on the notion of {\em resolvant} theories are used to derive new matching and in some cases unification procedures for a number of equational theories. Finally the combination of resolvant systems is investigated.



@inproceedings{Nipkow-LICS90, author="Tobias Nipkow", title="Proof Transformations for Equational Theories", booktitle="Proc.\ 5th IEEE Symp.\ Logic in Computer Science", year=1990,pages="278--288"}