Rigid E-Unification Revisited

Presented at CADE'00, Pittsburgh, PA, June 2000. © Springer-Verlag.

---

Authors

Ashish Tiwari, Leo Bachmair, and Harald Rueß

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 syntacticunification 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}
}

---

Harald Ruess: ruess@csl.sri.com