scientific article; zbMATH DE number 18651
From MaRDI portal
Publication:3976057
[For the entire collection see Zbl 0731.00025.] The authors introduce a new order proving termination of rewrite systems that are appropriate for associative-commutative (AC) operations. As shown by a number of examples, termination can be now established for a larger class of AC rewriting systems than one can do using, say, lexicographic recursive path ordering. Their method does not impose any restriction on the precedence relation for function symbols.
Recommendations
- A path ordering for proving termination of AC rewrite systems
- scientific article; zbMATH DE number 4047066
- A total, ground path ordering for proving termination of AC-rewrite systems
- AC-termination of rewrite systems: a modified Knuth-Bendix ordering
- Termination orderings for associative-commutative rewriting systems
Cited in
(15)- Associative-commutative reduction orderings
- Conditional narrowing modulo a set of equations
- Automated proofs of equality problems in Overbeek's competition
- Termination modulo equations by abstract commutation with an application to iteration
- A fully syntactic AC-RPO.
- Termination of rewrite systems by elementary interpretations
- A path ordering for proving termination of AC rewrite systems
- scientific article; zbMATH DE number 4047066 (Why is no real title available?)
- A total, ground path ordering for proving termination of AC-rewrite systems
- Any ground associative-commutative theory has a finite canonical system
- A precedence-based total AC-compatible ordering
- More problems in rewriting
- AC-termination of rewrite systems: a modified Knuth-Bendix ordering
- Path orderings for termination of associative-commutative rewriting
- A total AC-compatible ordering based on RPO
This page was built for publication:
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3976057)
