Logic in Computer Science (LICS 1988)

Paper: Proof by consistency in equational theories (at LICS 1988)

Authors: Leo Bachmair

Abstract

A method is proven for proving that equations are valid in the initial model of an equational variety. This proof by consistency procedure can be applied to equational theories that are represented as ground convergent rewrite systems. In contrast with so-called inductive completion procedures, the method requires no specific ordering on terms and can handle unorientable equations. The method is linear and refutationally complete, in that it refutes any equation which is not an inductive theorem

BibTeX

  @InProceedings{Bachmair-Proofbyconsistencyi,
    author = 	 {Leo Bachmair},
    title = 	 {Proof by consistency in equational theories},
    booktitle =  {Proceedings of the Third Annual IEEE Symp. on Logic in Computer Science, {LICS} 1988},
    year =	 1988,
    editor =	 {Yuri Gurevich},
    month =	 {July}, 
    pages =      {228--233},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}
  }