Lics

IEEE Symposium on Logic in Computer Science

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

Ninth Annual IEEE Symposium on

Logic in Computer Science (LICS 1994)

Paper: Normalised rewriting and normalised completion (at LICS 1994)

Authors: Claude Marché

Abstract

Introduces normalised rewriting, a new rewrite relation. It generalises former notions of rewriting modulo E, dropping some conditions on E. For example, E can now be the theory of identity, idempotency, the theory of Abelian groups, or the theory of commutative rings. We give a new completion algorithm for normalised rewriting. It contains as an instance the usual AC completion algorithm (AC being the set of equations containing the associativity and commutativity axioms), but also the well-known Buchberger's algorithm for computing standard bases of polynomial ideals. We investigate the particular case of completion of ground equations. In this case, we prove by a uniform method that completion modulo E terminates, for some interesting E. As a consequence, we obtain the decidability of the word problem for some classes of equational theories. We give implementation results which show the efficiency of normalised completion with respect to completion modulo AC

BibTeX

  @InProceedings{March-Normalisedrewriting,
    author = 	 {Claude Marché},
    title = 	 {Normalised rewriting and normalised completion},
    booktitle =  {Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS 1994)},
    year =	 {1994},
    month =	 {July}, 
    pages =      {394--403},
    location =   {Paris, France}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski