Unification of quantified terms

Abstract

Unification algorithms for quantified terms are needed for the implementation of extended functional and logic programming languages, and also for the implementation of other symbolic computation systems such as theorem provers and proof editors. This paper describes and proves correct such a unification algorithm. Although discussed here in a theoretically convenient way, the algorithm is suitable for enhancement of conventional unification algorithms for free variable terms, such as are found in, for example, Prolog interpreters. The algorithm has been demonstrated by modifying a conventional Prolog interpreter so as to interpret formulas which include previously declared quantifiers.