A Complete Unification Algorithm for Associative-Commutative Functions
Abstract
An important component of mechanical theorem proving systems are unification algorithms which find most genaral substitutions which, when applied to two expresssions, maka them equivalent. Functions which are associative 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 associativa and commutative is presented here The algorithm eliminates the need for axiomatizing the associativity and commutativity properties and returns a complete set of unifiers without recourse to the indefinite generation of vurianU and instances of the terms being unified required by previous solutions to the problem.
Cite
Text
Stickel. "A Complete Unification Algorithm for Associative-Commutative Functions." International Joint Conference on Artificial Intelligence, 1975. doi:10.21236/ada015846Markdown
[Stickel. "A Complete Unification Algorithm for Associative-Commutative Functions." International Joint Conference on Artificial Intelligence, 1975.](https://mlanthology.org/ijcai/1975/stickel1975ijcai-complete/) doi:10.21236/ada015846BibTeX
@inproceedings{stickel1975ijcai-complete,
title = {{A Complete Unification Algorithm for Associative-Commutative Functions}},
author = {Stickel, Mark E.},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1975},
pages = {71-76},
doi = {10.21236/ada015846},
url = {https://mlanthology.org/ijcai/1975/stickel1975ijcai-complete/}
}