Unification with ICSIM

This document describes the implementation of a distributed unification algorithm using the connectionist simulator ICSIM. The algorithm is based on S. Hoelldobler's work, as described in [Hoelldobler, 1990b]. Unification problems are specified according to a simple language, describing the terms, functions, variables and constants occurring in such a problem; the terms to be unified are represented as less than term_1 = term_2 is greater than (e.g., less than f(x, x, x) = f(g(a), y, g(z)) is greater than).A parser extracts relevant information and creates intermediate data structures needed for the construction of the connectionist network. Essential data structures describe the symbols occurring in the terms, the hierarchical structure of the terms (functions and their arguments), and the occurrences of the symbols in the terms. The connectionist unification network is constructed based on these intermediate structures. It is hierarchically organized, its top level NET consisting of POSITIONS, which correspond to the nodes in the term structure. A POSITION consists of a SYMBOL, either of type VARIABLE or CONSTANT. Symbols comprise a TERM UNIT and a number of UNIFICATION UNITS, depending on the number of positions in the terms to be unified. Initially, TERM UNITS are set according to the occurrences of their symbols in the term structure; based on the links within the network and the activation of UNIFICATION UNITS, more TERM UNITS are activated as required by the unification algorithm. The final set of active TERM UNITS is used to construct the most general unifier for the terms to be unified. The network can be easily extended to detect inconsistencies in the term structure or to perform an occur check.

ICSI Technical Report TR-91-053

Technical Report