Proof transformations for equational theories

Publikation: Beitrag in Buch/Bericht/KonferenzbandKonferenzbeitragBegutachtung

19 Zitate (Scopus)


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.

TitelComputer Science
Herausgeber (Verlag)Publ by IEEE
ISBN (Print)0818620730
PublikationsstatusVeröffentlicht - 1990
Extern publiziertJa
VeranstaltungProceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science - Philadelphia, PA, USA
Dauer: 4 Juni 19907 Juni 1990


NameProceedings - Symposium on Logic in Computer Science


KonferenzProceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science
OrtPhiladelphia, PA, USA


Untersuchen Sie die Forschungsthemen von „Proof transformations for equational theories“. Zusammen bilden sie einen einzigartigen Fingerprint.

Dieses zitieren