UNIMOK: a system for combining equational unification algorithms

摘要

Equational unification algorithms can be sued in resolution based theorem provers [9] and rewriting engines [6] to improve their handling of equality.Originally,the requirements of these theorem provers and rewrite engines were such that the unification algorithms had to compute complete sets of unifiers.But with the advent of constraint based approaches to theorem proving [4] and rewriting [8] the interest in unification algorithm that worked merely as decision procedures grew because minimal complete sets of unifiers can be very large - e.g.,doubly exponential in the number of variables of the problem in the case of the theory AC - and are hence costly to compute.