Path Orderings for Termination of Associative-Commutative Rewriting

13 years 8 months ago

Download www.cs.tau.ac.il

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.

Nachum Dershowitz, Subrata Mitra

Real-time Traffic

Binary Path Condition | CTRS 1992 | Recursive Path | Theoretical Computer Science |

claim paper

» A Maude Coherence Checker Tool for Conditional OrderSorted Rewrite Theories

» Automation of Recursive Path Ordering for Infinite Labelled Rewrite Systems

» Recursive Path Orderings Can Also Be Incremental

» The HigherOrder Recursive Path Ordering

» Proving Termination Using Recursive Path Orders and SAT Solving

» HigherOrder Critical Pairs

» Orderings for Innermost Termination

» POP and Semantic Labeling Using SAT

Post Info
More Details (n/a)

Added	10 Aug 2010
Updated	10 Aug 2010
Type	Conference
Year	1992
Where	CTRS
Authors	Nachum Dershowitz, Subrata Mitra

Comments (0)

Sciweavers

Path Orderings for Termination of Associative-Commutative Rewriting

Binary Path Condition | CTRS 1992 | Recursive Path | Theoretical Computer Science |

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers