Lecture Notes in Artificial Intelligence, Volume 1831.
From Automated Deduction CADE-17.
Edited by David McAllester.
Springer-Verlag, Pittsburgh, PA.
June, 2000.
Pages 220–234.

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.

@inproceedings{Tiwari-etal00:CADE,
    AUTHOR = {Ashish Tiwari and Leo Bachmair and Harald Rue\ss},
    TITLE = {Rigid E-Unification Revisited},
    BOOKTITLE = {Automated Deduction {CADE-17}},
    YEAR = {2000},
    EDITOR = {David McAllester},
    SERIES = {Lecture Notes in Artificial Intelligence},
    VOLUME = {1831},
    PAGES = {220--234},
    ADDRESS = {Pittsburgh, {PA}},
    MONTH = {jun},
    PUBLISHER = {Springer-Verlag},
    URL = {http://www.csl.sri.com/papers/tiwari-cade/}
}

• cade00-REU.ps.gz