Paper: Orderings for Equational Proofs (at LICS 1986)

Authors: Leo Bachmair Nachum Dershowitz Jieh Hsiang

Abstract

In this paper we introduce a new technique -orderings for equational proofs- for establishing completeness of equational proof theories. We study methods for constructing canonical rewrite systems for equational theories and apply our technique to the standard Knuth-Bendix completion method and to extensitions of completion to rewriting modulo a congruence. We present new and improved completion procedures and corresponding correctness proofs that are simple and intuitive. In addition, we describe extensions of completion that always succeed in constructing a canonical system for a given set of equations, whenever such a system exists at all. These unfailing completion procedures may also be used for refutational theorem proving in equational theories.

BibTeX

  @InProceedings{BachmairDershowitzH-OrderingsforEquatio,
    author = 	 {Leo Bachmair and Nachum Dershowitz and Jieh Hsiang},
    title = 	 {Orderings for Equational Proofs},
    booktitle =  {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)},
    year =	 {1986},
    month =	 {June}, 
    pages =      {346--357},
    location =   {Cambridge, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }