Sciweavers

FSTTCS
2001
Springer

Rewrite Closure for Ground and Cancellative AC Theories

14 years 2 months ago
Rewrite Closure for Ground and Cancellative AC Theories
Given a binary relation IE ∪ IR on the set of ground terms e signature, we define an abstract rewrite closure for IE ∪ IR. act rewrite closure can be interpreted as a specialized ground tree transducer (pair of bottom-up tree automata) and can be used to efficiently decide the reachability relation →∗ IE∪IE−∪IR. It is constructed using a completion like procedure. Correctness is established using proof ordering techniques. The procedure is extended, in a modular way, to deal with signatures containing cancellative associative commutative function symbols.
Ashish Tiwari
Added 28 Jul 2010
Updated 28 Jul 2010
Type Conference
Year 2001
Where FSTTCS
Authors Ashish Tiwari
Comments (0)