Normalization via Rewrite Closures

L. Bachmair, C. R. Ramakrishnan, I. V. Ramakrishnan and A. Tiwari

Presented at Rewriting Techniques and Applications, RTA-1999 , Trento, Italy, July 1999. © Springer-Verlag. The final version will be available at the Springer LNCS site

Abstract

We present an abstract completion-based method for finding normal forms of terms with respect to given rewrite systems. The method uses the concept of a rewrite closure, which is a generalization of the idea of a congruence closure. Our results generalize previous results on congruence closure-based normalization methods. The description of known methods within our formalism also allows a better understanding of these procedures.

gzipped postscript or postscript

BibTeX Entry


@inproceedings{BRRT99:RTA,
	TITLE = {Normalization via Rewrite Closures},
	AUTHOR = {L. Bachmair and C.R. Ramakrishnan and I.V.Ramakrishnan and A. Tiwari},
	BOOKTITLE = {Rewriting Techniques and Applications, RTA 1999},
	EDITOR = {P. Narendran and M. Rusinowitch},
	PAGES = {190--204},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	VOLUME = 1631,
	MONTH = jul,
	YEAR = 1999,
	ADDRESS = {Trento, Italy}
}
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page