Proof transformations for equational theories

Author

Nipkow, Tobias

Author_Institution

Comput. Lab., Cambridge Univ., UK

fYear

1990

fDate

4-7 Jun 1990

Firstpage

278

Lastpage

288

Abstract

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

Keywords

equivalence classes; rewriting systems; theorem proving; associativity plus commutativity; decision procedures; equational logic; equational theories; equivalence tests; matching algorithms; proof systems; proof transformation; proof translations; resolvent systems; rewriting systems; unification procedures; Contracts; Decision feedback equalizers; Equations; Laboratories; Logic; Monitoring; System testing;

fLanguage

English

Publisher

ieee

Conference_Titel

Logic in Computer Science, 1990. LICS '90, Proceedings., Fifth Annual IEEE Symposium on e

Conference_Location

Philadelphia, PA

Print_ISBN

0-8186-2073-0

Type

conf

DOI

10.1109/LICS.1990.113754

Filename

113754