Termination of rewriting
type: Item
instance of: scholarly article
title: Termination of rewriting
zbMATH Open document ID: 0637.68035
DOI: 10.1016/S0747-7171(87)80022-6
author: Nachum Dershowitz
published in: Journal of Symbolic Computation
publication date: 1987-01-01T00:00:00Z
review text: This survey describes methods for proving that systems of rewrite rules are terminating programs. We illustrate the use in termination proofs of various kinds of orderings on terms, including polynomial interpretations and path orderings. The effect of restrictions, such as linearity, on the form of rules is also considered. In general, however, termination is an undecidable property of rewrite systems.
Mathematics Subject Classification ID: 68Q65
Mathematics Subject Classification ID: 68W30
zbMATH DE Number: 4039278
zbMATH Keywords: term rewriting
zbMATH Keywords: survey
zbMATH Keywords: rewrite rules
zbMATH Keywords: termination proofs
zbMATH Keywords: orderings on terms
Wikidata QID: Q56814378
describes a project that uses: REVE
describes a project that uses: RRL
MaRDI profile type: Publication
cites work: Konstruktiver Aufbau eines Abschnitts der zweiten Cantorschen Zahlenklasse
cites work: Q3700828
cites work: Termination orderings for associative-commutative rewriting systems
cites work: Q3783521
cites work: Q3757390
cites work: Q3783523
cites work: Q3657410
cites work: Q3851592
cites work: Q3318040
cites work: Decision procedures for real and p‐adic fields
cites work: Q4079605
cites work: Q3702507
cites work: A note on simplification orderings
cites work: Q3917482
cites work: Orderings for term-rewriting systems
cites work: Q4385532
cites work: Proving termination with multiset orderings
cites work: Q3912031
cites work: Q3696498
cites work: On regularity of context-free languages
cites work: Systems of predicative analysis, II: Representations of ordinals
cites work: Q3783522
cites work: On Proving Uniform Termination and Restricted Termination of Rewriting Systems
cites work: Another generalization of Higman's well quasi order result on \(\Sigma ^*\)
cites work: Ordering by Divisibility in Abstract Algebras
cites work: Q3674088
cites work: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
cites work: Q3883561
cites work: Q3327710
cites work: Completion of a Set of Rules Modulo a Set of Equations
cites work: On multiset orderings
cites work: Q3659124
cites work: Q3336736
cites work: Q3683533
cites work: Extensions of arithmetic for proving termination of computations
cites work: Accessible Independence Results for Peano Arithmetic
cites work: Q3922646
cites work: Q5585020
cites work: Q5581665
cites work: Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture
cites work: The theory of well-quasi-ordering: a frequently discovered concept
cites work: New decision algorithms for finitely presented commutative semigroups
cites work: Q3890740
cites work: Q3667939
cites work: Q3336681
cites work: Q3664414
cites work: Q4195948
cites work: Q4772698
cites work: Q4124327
cites work: Extension functions for multiset orderings
cites work: About the rewriting systems produced by the Knuth-Bendix completion algorithm
cites work: Calcul de longueurs de chaînes de réécriture dans le monoïde libre
cites work: Q5734436
cites work: Q5520569
cites work: On theories with a combinatorial definition of 'equivalence'
cites work: Computing in systems described by equations
cites work: Q3786478
cites work: Constructing recursion operators in intuitionistic type theory
cites work: A property which guarantees termination in weak combinatory logic and subtree replacement systems

Termination of rewriting (cites work)
cites work: Q3930625

Termination of rewriting (cites work)
cites work: The undecidability of self-embedding for term rewriting systems

Termination of rewriting (cites work)
cites work: Q3783520

Termination of rewriting (cites work)
cites work: Q3696524

Termination of rewriting (cites work)
cites work: Q3783524

Termination of rewriting (cites work)
cites work: Q3711760

Termination of rewriting (cites work)
cites work: Partial well‐ordering of sets of vectors

Termination of rewriting (cites work)
cites work: Operational and Semantic Equivalence Between Recursive Programs

Termination of rewriting (cites work)
cites work: Tree-Manipulating Systems and Church-Rosser Theorems

Termination of rewriting (cites work)
cites work: Q3696501

Termination of rewriting (cites work)
cites work: Q5344167

Termination of rewriting (cites work)
cites work: Nichtbeweisbarkeit von gewissen kombinatorischen Eigenschaften endlicher Bäume;Unprovability of certain combinatorial properties of finite trees

Termination of rewriting (cites work)
cites work: Automated Theorem-Proving for Theories with Simplifiers Commutativity, and Associativity

Termination of rewriting (cites work)
cites work: TREES AND BALL GAMES

Termination of rewriting (cites work)
cites work: Q3262873

Termination of rewriting (cites work)
cites work: Q5807665

Termination of rewriting (cites work)
cites work: Q3698786

Termination of rewriting (cites work)
cites work: On the Church-Rosser property for the direct sum of term rewriting systems

Termination of rewriting (DBLP publication ID)
DBLP publication ID: journals/jsc/Dershowitz87