On determining the causes of nonunifiability

AbstractDetermining whether or not a set of constraints (pairs of functional expressions) is unifiable is a key problem in mechanical theorem proving, in particular logic programming, the most significant application of mechanical theorem proving techniques to date. A related problem of considerable importance is what to do when unification fails. The usual strategy employed by logic programming interpreters is to backtrack to the last point at which an alternative clause can be applied. This may not be the correct place to resume the search, however, and although the correct backtracking point will eventually be found, innocuous parts of the proof will be repeatedly destroyed and rebuilt in the process. We present a method for determining all maximal unifiable subsets of a set of constraints, information which can be used as a basis for more intelligent backtracking behavior