Rewrite Closures for Ground and Cancellative AC Theories

Rewrite Closures for Ground and Cancellative AC Theories

Ashish Tiwari

To be presented at FST&TCS'01, IISc Bangalore, India, Dec 13--15 2001. © Springer-Verlag. The final version will be available at the Springer LNCS site

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.

pdf

Full version can be downloaded from here .

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,
	ADDRESS = {IISc, Bangalore}
}

Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page