Difference Unification
Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence. Automated Reasoning. Pages 116-121.
Abstract
We extend work on difference identification and reduction as a technique for automated reasoning. We generalise 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 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 for efficiently applying these rules. 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.
@inproceedings{ijcai1993p17,
title = {Difference Unification},
author = {Basin, David A. and Walsh, Toby},
booktitle = {Proceedings of the Thirteenth International Joint Conference on
Artificial Intelligence, {IJCAI-93}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Ruzena Bajcsy},
pages = {116--121},
year = {1993},
note = {Automated Reasoning},
url = {https://ijcai.org/proceedings/1993/17},
}
TY - CPAPER TI - Difference Unification AU - Basin, David A. AU - Walsh, Toby T2 - Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence, IJCAI-93 PB - International Joint Conferences on Artificial Intelligence PY - 1993 SP - 116 EP - 121 UR - https://ijcai.org/proceedings/1993/17 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
