---
title: "A Unification Algorithm for Infinite Trees"
authors:
  - "Kuniaki Mukai"
doi: ""
url: "https://ijcai.org/proceedings/1983/131"
pdf: "https://ijcai.org/proceedings/1983/0131.pdf"
venue: "Proceedings of the Eighth International Joint Conference on Artificial Intelligence"
year: 1983
pages: "547-548"
track: "Logic Programming"
keywords:
---

# A Unification Algorithm for Infinite Trees

Kuniaki Mukai

*Proceedings of the Eighth International Joint Conference on Artificial Intelligence*, pages 547-548.

## Abstract

A simple unification algorithm for infinite trees has been developed. The algorithm i s designed to work efficiently under structure sh a ring implementa tions of logic programming languages, e.g., Prolog (Warren [3)). A relation, called "is covered with", betw ee n two terms is introduced to terminate the a lgorithm. The fund a mental operations are to comp ute the frontier set of two given terms and to test the relation between them. A termination proof is shown.