TY - GEN

T1 - Proof transformations for equational theories

AU - Nipkow, Tobias

PY - 1990

Y1 - 1990

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

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

UR - http://www.scopus.com/inward/record.url?scp=0025645111&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:0025645111

SN - 0818620730

T3 - Proceedings - Symposium on Logic in Computer Science

SP - 278

EP - 288

BT - Computer Science

PB - Publ by IEEE

T2 - Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science

Y2 - 4 June 1990 through 7 June 1990

ER -