Path Orderings for Termination of Associative-Commutative Rewriting

We show that a simple, and easily implementable, restriction on the recursive path ordering, which we call the "binary path condition," sufficesfor establishing termination of extended rewriting modulo associativity and commutativity.

• Type: Conference
• Year: 1992
• Where: CTRS
• Authors: Nachum Dershowitz, Subrata Mitra
• Keywords: Binary Path Condition, CTRS 1992, Recursive Path, Theoretical Computer Science