A higher order logic unification algorithm

The present work resulted from an HOL (higher order logic) interpreter prototype called λ-PROLOG. Only positive definite sentences are used in the language. They are similar to those of the first order logic programming language and present some appropriate mechanization properties. Unification is the most important interpreter procedure and has high complexity. Its processing is one of the reasons for the impoverishment of system quality. In the present work, analyses of the MATCH and SIMPL algorithms that were developed for this purpose are used to supply a new form algorithm which, in contrast to MATCH, shows initial performance gains and an easier procedural interpretation of the unification mechanism