A Complete Unification Algorithm for Associative-Commutative Functions
Proceedings of the Fourth International Joint Conference on Artificial Intelligence. Mathematical and Theoretical Aspects of A.I. Pages 71-75.
Abstract
An important component of mechanical theorem provinc systems are unification algorithms which find most general sul!stitutions which, when applied to two expresssions, make them equivalent. Functions which are associat i ve and commutative (such as the arithmetic addition and multiplication functions) are often the subject of mechanical theorem proving . An algorithm which unifies terms whose function is associative and commutative is presented here. The algorithm eliminates the need for axiomatizing the usoeiativity and commutativity properties and returns 1 complete set of unifiers without recourse to the · indefinite generation of variants and instances of the terms beinc unified required by previous solutions to the problem.
@inproceedings{ijcai1975p12,
title = {A Complete Unification Algorithm for Associative-Commutative Functions},
author = {Stickel, Mark E.},
booktitle = {Proceedings of the Fourth International Joint Conference on
Artificial Intelligence, {IJCAI-75}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Patrick Winston and Carl Hewitt},
pages = {71--75},
year = {1975},
note = {Mathematical and Theoretical Aspects of A.I},
url = {https://ijcai.org/proceedings/1975/12},
}
TY - CPAPER TI - A Complete Unification Algorithm for Associative-Commutative Functions AU - Stickel, Mark E. T2 - Proceedings of the Fourth International Joint Conference on Artificial Intelligence, IJCAI-75 PB - International Joint Conferences on Artificial Intelligence PY - 1975 SP - 71 EP - 75 UR - https://ijcai.org/proceedings/1975/12 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
