Technical reports

Proof transformations for equational theories

Tobias Nipkow

September 1989, 17 pages

DOI: 10.48456/tr-181

Abstract

This paper 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.

Two new matching alogorithms for (among other theories) associativity, associativity + commutativity, and associativity + commutativity + identity are presented, 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 studying proof translations defined by rewriting systems, equivalence tests based on the notion of resolvant theories are used to derive new matching and in some cases unification procedures for a number of equational theories. Finally the combination of resolvant systems is investigated.

Full text

PDF (1.1 MB)

BibTeX record

@TechReport{UCAM-CL-TR-181,
  author =	 {Nipkow, Tobias},
  title = 	 {{Proof transformations for equational theories}},
  year = 	 1989,
  month = 	 sep,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-181.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-181},
  number = 	 {UCAM-CL-TR-181}
}