Rewrite Closures for Ground and Cancellative AC Theories

### Abstract

Given a binary relation $\inputeqns\cup\inputrules$ on the set of ground terms over some signature, we define an abstract rewrite closure for $\inputeqns\cup\inputrules$. An abstract 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 $\rightarrow_{\inputeqns\cup\inputeqns^{-}\cup\inputrules}^*$. 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.

#### Slides

gzipped postscript or postscript

#### BibTeX Entry


@inproceedings{Tiw01:FSTTCS,
TITLE = {Rewrite Closures for Ground and Cancellative AC Theories},
AUTHOR = {A. Tiwari},
BOOKTITLE = {Foundations of Software Technology and Theoretical Computer Science, FST\&TCS 2001},
EDITOR = {Hariharan, R. and Mukund, M. and Vinay, V.},
PAGES = {334--346},
PUBLISHER = {Springer-Verlag},
SERIES = {Lecture Notes in Computer Science},
VOLUME = 2245,
MONTH = dec,
YEAR = 2001,