Proof transformations for equational theories

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

19 Scopus citations


This study 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. Novel matching algorithms for (among other theories) associativity, associativity plus commutativity, and associativity plus commutativity plus identity are presented, but 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 a study of proof translations defined by rewriting systems, equivalence tests based on the notion of resolvent theories are used to derive novel matching and, in some cases unification procedures for a number of equational theories. The combination of resolvent systems is investigated.

Original languageEnglish
Title of host publicationComputer Science
PublisherPubl by IEEE
Number of pages11
ISBN (Print)0818620730
StatePublished - 1990
Externally publishedYes
EventProceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science - Philadelphia, PA, USA
Duration: 4 Jun 19907 Jun 1990

Publication series

NameProceedings - Symposium on Logic in Computer Science


ConferenceProceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science
CityPhiladelphia, PA, USA


Dive into the research topics of 'Proof transformations for equational theories'. Together they form a unique fingerprint.

Cite this