Rigid E-Unification Revisited

Ashish Tiwari, Leo Bachmair and Harald Ruess

Presented at CADE'00, Pittsburgh, PA, June 2000. © Springer-Verlag. The final version will be available at the Springer LNCS site

Abstract

This paper presents a sound and complete set of abstract transformation rules for rigid $E$-unification. Abstract congruence closure, syntactic unification and paramodulation are the three main components of the proposed method. The method obviates the need for using any complicated term orderings and easily incorporates suitable optimization rules. Characterization of substitutions as congruences allows for a comparatively simple proof of completeness using proof transformations. When specialized to syntactic unification, we obtain a set of abstract transition rules that describe a class of efficient syntactic unification algorithms.

gzipped postscript or postscript

BibTeX Entry


@inproceedings{TiwariBachmairRuess00:CADE,
	TITLE = {Rigid E-Unification Revisited},
	AUTHOR = {Ashish Tiwari and Leo Bachmair and Harald Ruess},
	BOOKTITLE = {Conference on Automated Deduction, CADE '2000},
	EDITOR = {David McAllester},
	PAGES = {220--234},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Artificial Intelligence},
	VOLUME = 1831,
	MONTH = jun,
	YEAR = 2000,
	ADDRESS = {Pittsburgh, PA}
}
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page