Termination orderings for associative-commutative rewriting systems

DOI10.1016/S0747-7171(85)80019-5zbMath0587.68041MaRDI QIDQ1072371

Leo Bachmair, David Alan Plaisted

Publication date: 1985

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

term rewriting systemsequational theoryassociative path orderingsprecedence orderingsimplification orderings

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Related Items (27)

Path orderings for termination of associative-commutative rewriting ⋮ Fracpairs and fractions over a reduced commutative ring ⋮ A path ordering for proving termination of AC rewrite systems ⋮ A precedence-based total AC-compatible ordering ⋮ Extension of the associative path ordering to a chain of associative commutative symbols ⋮ Termination of rewriting ⋮ History and basic features of the critical-pair/completion procedure ⋮ Modular and incremental proofs of AC-termination ⋮ Elimination transformations for associative-commutative rewriting systems ⋮ AC-Termination of rewrite systems: A modified Knuth-Bendix ordering ⋮ Buchberger's algorithm: A constraint-based completion procedure ⋮ Termination modulo equations by abstract commutation with an application to iteration ⋮ AC-KBO revisited ⋮ A fully syntactic AC-RPO. ⋮ A rewriting strategy to verify observational congruence ⋮ A total AC-compatible ordering based on RPO ⋮ Theorem proving in cancellative abelian monoids (extended abstract) ⋮ Associative-commutative reduction orderings ⋮ Termination and completion modulo associativity, commutativity and identity ⋮ Any ground associative-commutative theory has a finite canonical system ⋮ Completion of rewrite systems with membership constraints ⋮ Termination of rewrite systems by elementary interpretations ⋮ Conditional narrowing modulo a set of equations ⋮ Completion for rewriting modulo a congruence ⋮ Forward analysis for WSTS, part I: completions ⋮ Superposition theorem proving for abelian groups represented as integer modules ⋮ Knuth-Bendix Completion for Non-Symmetric Transitive Relations

Uses Software

• RRL
• REVE

Cites Work

• Orderings for term-rewriting systems
• Refutational theorem proving using term-rewriting systems
• A note on simplification orderings
• Computing with rewrite systems
• Proving termination with multiset orderings
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Complete Sets of Reductions for Some Equational Theories
• Abstract data types and software validation
• Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Termination orderings for associative-commutative rewriting systems