A Unification Algorithm for Infinite Trees
Abstract
A simple unification algorithm for infinite trees has been developed. The algorithm designed to work efficiently under structure sharing implementations of logic programming languages, e.g., Prolog (Warren [3]). A relation, called is covered with, between two terms introduced to terminate the algorithm. The fundamental operations are to compute the frontier set of two given terms and to test the relation between them. A termination proof shown.
Cite
Text
Mukai. "A Unification Algorithm for Infinite Trees." International Joint Conference on Artificial Intelligence, 1983.Markdown
[Mukai. "A Unification Algorithm for Infinite Trees." International Joint Conference on Artificial Intelligence, 1983.](https://mlanthology.org/ijcai/1983/mukai1983ijcai-unification/)BibTeX
@inproceedings{mukai1983ijcai-unification,
title = {{A Unification Algorithm for Infinite Trees}},
author = {Mukai, Kuniaki},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1983},
pages = {547-549},
url = {https://mlanthology.org/ijcai/1983/mukai1983ijcai-unification/}
}