Termination orderings for associative-commutative rewriting systems
type: Item
instance of: scholarly article
title: Termination orderings for associative-commutative rewriting systems
zbMATH Open document ID: 0587.68041
DOI: 10.1016/S0747-7171(85)80019-5
author: Leo Bachmair
author: David A. Plaisted
published in: Journal of Symbolic Computation
publication date: 1985-01-01T00:00:00Z
review text: In this paper we describe a new class of orderings - associative path orderings - for proving termination of associative-commutative term rewriting systems. These orderings are based on the concept of simplification orderings and extend the well-known recursive path orderings to E-congruence classes, where E is an equational theory consisting of associativity and commutativity axioms. Associative path orderings are applicable to term rewriting systems for which a precedence ordering on the set of operator symbols can be defined that satisfies a certain condition, the associative path condition. These precedence ordering can often be derived from the structure of the reduction rules. We include termination proofs for various term rewriting systems (for rings, Boolean algebra, etc.) and, in addition, point out ways to handle situations where the associative path condition is too restrictive.
Mathematics Subject Classification ID: 68W30
zbMATH DE Number: 3943026
zbMATH Keywords: associative path orderings
zbMATH Keywords: simplification orderings
zbMATH Keywords: equational theory
zbMATH Keywords: term rewriting systems
zbMATH Keywords: precedence ordering
describes a project that uses: REVE
describes a project that uses: RRL
MaRDI profile type: Publication
cites work: Q3783521
cites work: A note on simplification orderings
cites work: Orderings for term-rewriting systems
cites work: Q3703288
cites work: Computing with rewrite systems
cites work: Proving termination with multiset orderings
cites work: Abstract data types and software validation
cites work: Refutational theorem proving using term-rewriting systems
cites work: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
cites work: Q3659124
cites work: Q3336736
cites work: Q3683533
cites work: Q5581665
cites work: Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture
cites work: Q3667939
cites work: Complete Sets of Reductions for Some Equational Theories
cites work: Q3696501
Recommended article: Path orderings for termination of associative-commutative rewriting
Recommended article: A termination ordering for higher order rewrite systems
Recommended article: Q4035223
Recommended article: Q3783522
Recommended article: AC-Termination of rewrite systems: A modified Knuth-Bendix ordering
Recommended article: Q3683533
Recommended article: Q4503901
Recommended article: Q3336681
Recommended article: Term orderings for non-reachability of (conditional) rewriting
Recommended article: Q3830525
description: scientific article; zbMATH DE number 3943026