Skip to main navigation Skip to search Skip to main content

A path ordering for proving termination of term rewriting systems

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

25 Scopus citations

Abstract

A new partial ordering scheme for proving uniform termination of term rewriting systems is presented. The basic idea is that two terms are compared by comparing the paths through them. It is shown that the ordering is a well-founded simplification ordering and also a strict extension of the recursive path ordering scheme of Dershowitz. Terms can be compared under this path ordering in polynomial time.

Original languageEnglish
Title of host publicationMathematical Foundations of Software Development
Subtitle of host publicationProceedings of the International Joint Conference on Theory and Practice of Software Development, TAPSOFT - Colloquium on Trees in Algebra and Programming CAAP 1985
EditorsJames Thatcher, Hartmut Ehrig, Christiane Floyd, Maurice Nivat
PublisherSpringer Verlag
Pages173-187
Number of pages15
ISBN (Print)9783540151982
DOIs
StatePublished - 1985
EventInternational Joint Conference on Theory and Practice of Software Development, TAPSOFT 1985 - Berlin, Germany
Duration: Mar 25 1985Mar 29 1985

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume185 LNCS

Conference

ConferenceInternational Joint Conference on Theory and Practice of Software Development, TAPSOFT 1985
Country/TerritoryGermany
CityBerlin
Period03/25/8503/29/85

Fingerprint

Dive into the research topics of 'A path ordering for proving termination of term rewriting systems'. Together they form a unique fingerprint.

Cite this