Ordered rewriting and confluence

Ursula Martin, Tobias Nipkow

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

33 Scopus citations


One of the major problems in term rewriting theory is what to do with an equation which cannot be ordered into a rule. Many solutions have been proposed, including the use of special unification algorithms or of unfailing completion procedures. If an equation cannot be ordered we can still use any instances of it which can be ordered for rewriting. Thus for example x*y=y*x cannot be ordered, but if a,b are constants with b*a>a*b we may rewrite b*a → a*b. This idea is used in unfailing completion, and also appears in the Boyer-Moore system. In this paper we define and investigate completeness with respect to this notion of rewriting and show that many familiar systems are complete rewriting systems in this sense. This allows us to decide equality without the use of special unification algorithms. We prove completeness by proving termination and local confluence. We describe a confluence test based on recursive properties of the ordering.

Original languageEnglish
Title of host publication10th International Conference on Automated Deduction, Proceedings
EditorsMark E. Stickel
PublisherSpringer Verlag
Number of pages15
ISBN (Print)9783540528852
StatePublished - 1990
Externally publishedYes
Event10th International Conference on Automated Deduction, CADE 1990 - Kaiserslautern, Germany
Duration: 24 Jul 199027 Jul 1990

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume449 LNAI
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference10th International Conference on Automated Deduction, CADE 1990


Dive into the research topics of 'Ordered rewriting and confluence'. Together they form a unique fingerprint.

Cite this