#### 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.

dvi

BibTeX:

@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"}