An Algorithm for the Retrieval of Unifiers from Discrimination Trees

    loading  Checking for direct PDF access through Ovid

Abstract

We present a modification of the unification algorithm that is adapted to the extraction of simultaneously unifiable literals from discrimination trees. The algorithm is useful for efficient implementation of binary resolution, hyperresolution, and paramodulation. The algorithm is able to traverse simultaneously more than one discrimination tree and to construct a unifier at the same time. In this way backtracking is reduced.

Related Topics

    loading  Loading Related Articles