A fully syntactic AC-RPO.

DOI10.1006/inco.2002.3158zbMath1049.68076OpenAlexW4213157689MaRDI QIDQ1400715

Albert Rubio

Publication date: 2002

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://semanticscholar.org/paper/7bb9a4389d04765ff256b6095abe39ae7c2b7bda

zbMATH Keywords

recursive path orderingterm orderings

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Related Items

Non-E-Overlapping, Weakly Shallow, and Non-Collapsing TRSs are Confluent ⋮ CoLL: A Confluence Tool for Left-Linear Term Rewrite Systems ⋮ AC-KBO revisited ⋮ Semantically-guided goal-sensitive reasoning: decision procedures and the Koala prover ⋮ Building Theorem Provers ⋮ Extending Maximal Completion (Invited Talk) ⋮ SGGS decision procedures

Uses Software

• REVE

Cites Work

• Termination of rewriting systems by polynomial interpretations and its implementation
• Orderings for term-rewriting systems
• A total AC-compatible ordering based on RPO
• Termination orderings for associative-commutative rewriting systems
• Associative-commutative reduction orderings
• A total, ground path ordering for proving termination of AC-rewrite systems
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item