ACM/IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Fifth Annual IEEE Symposium on

Logic in Computer Science (LICS 1990)

Paper: Proof transformations for equational theories (at LICS 1990)

Authors: Tobias Nipkow


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


    author = 	 {Tobias Nipkow},
    title = 	 {Proof transformations for equational theories},
    booktitle =  {Proceedings of the Fifth Annual IEEE Symposium on Logic in Computer Science (LICS 1990)},
    year =	 {1990},
    month =	 {June}, 
    pages =      {278--288},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}

Last modified: 2022-10-3113:49
Sam Staton