SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
     
  SRI Logo

Rigid E-Unification Revisited
 by Dr. Harald Rueß, Dr. Ashish Tiwari & Leo Bachmair.

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.


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.
BibTEX Entry
@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/}
}
Files
 













 

About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2017 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy