1990 | ReviewPaper | Buchkapitel
Ordered rewriting and confluence
verfasst von : Ursula Martin, Tobias Nipkow
Erschienen in: 10th International Conference on Automated Deduction
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.