IEEE Symposium on Logic in Computer Science

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

First Annual IEEE Symposium on

Logic in Computer Science (LICS 1986)

Paper: Orderings for Equational Proofs (at LICS 1986)

Winner of the Test-of-Time Award in 2006
Authors: Leo Bachmair Nachum Dershowitz Jieh Hsiang


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.


    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}

Last modified: 2016-01-1416:21
Andrzej Murawski