Difference Unification

Abstract

Responsibility for the contents of this publication lies with the authors. We thank the Edinburgh Mathematical Reasoning Group for their encouragement and criticism. In particular, we thank Alan Bundy, Andrew Ireland, Sean Matthews, and Andreas Tonne. We extend previous work on difference identification and reduction as a technique for automated reasoning. We generalize unication so that terms are made equal not only by nding substitutions for variables but also by hiding term structure. This anno-tation of structural differences serves to direct rippling, a kind of rewriting designed to remove structural dierences in a controlled way. On the technical side, we give a rule-based algorithm for difference unication, 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 ecient 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.