@INPROCEEDINGS{BasinWalsh93b,
AUTHOR        = {David Basin  and Toby Walsh},
TITLE         = {Difference Unification},
EDITOR        = {R.~Bajcsy},
BOOKTITLE     = {Proc.~13th Intern.~Joint Conference on Artificial  Intelligence
 (IJCAI '93)} # " {\rm (Chambery, France)}",
ADDRESS       = {San Mateo, CA},
PUBLISHER     = {Morgan Kaufmann},
YEAR          = {1993},
VOLUME        = {1},
PAGES         = {116--122},
NOTE          = {The paper available here is an extended version of the IJCAI paper.  If you wish to cite it, please use this bibtex entry for IJCAI paper.},
ABSTRACT      = {
We extend previous work on difference identification and
reduction as a technique for automated reasoning. We generalize
unification so that terms are made equal not only by finding
substitutions for variables but also by hiding term structure.
This annotation of structural differences serves to direct
rippling, a kind of rewriting designed to remove structural
differences in a controlled way. On the technical side,
we give a rule-based algorithm for difference unification,
and analyze its correctness, completeness, and complexity.
On the practical side, we present a novel search strategy
(called left-first search) for applying these rules in an
efficient way. Finally, we show how this algorithm can be
used in new ways to direct rippling and how it can play
an important role in theorem proving and other kinds of
automated reasoning.},
}