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.

• Type: Conference
• Year: 2001
• Where: FSTTCS
• Authors: Ashish Tiwari
• Keywords: Abstract Rewrite Closure, Binary Relation Ie, FSTTCS 2001, Rewrite Closure, Software Engineering