A total AC-compatible ordering based on RPO

DOI10.1016/0304-3975(94)00276-2zbMath0873.68102OpenAlexW1996023831MaRDI QIDQ673623

Albert Rubio, Robert Nieuwenhuis

Publication date: 28 February 1997

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(94)00276-2

zbMATH Keywords

AC-symbolsrewrite ryles

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Unification of infinite sets of terms schematized by primal grammars, A fully syntactic AC-RPO., Canonized Rewriting and Ground AC Completion Modulo Shostak Theories, Theorem proving in cancellative abelian monoids (extended abstract), AC-superposition with constraints: No AC-unifiers needed, Termination Modulo Combinations of Equational Theories

Uses Software

• REVE

Cites Work

• Termination of rewriting systems by polynomial interpretations and its implementation
• Termination orderings for associative-commutative rewriting systems
• Termination of rewriting
• Associative-commutative reduction orderings
• On ground AC-completion
• Any ground associative-commutative theory has a finite canonical system
• A precedence-based total AC-compatible ordering
• Extension of the associative path ordering to a chain of associative commutative symbols
• AC-superposition with constraints: No AC-unifiers needed
• SOLVING SYMBOLIC ORDERING CONSTRAINTS
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item