Intelligent backtracking in deduction systems by means of extended unification graphs (Q1101246)

A method for unification as the basis for intelligent backtracking in deduction systems is described. This method is based on the unification graphs introduced by Cox. In this paper, unification graphs are used in an extended form such that they represent all the information which can be gained from the unification constraints, i.e., the expression to be unified, their subterms which, as a consequence, are to be unified, the number of deduction steps which cause the unification of two terms, and the term-subterm relation as far as necessary. If a unification conflict occurs from this information, the deduction steps which have led to these conflicts can be determined and reset. This is done by searching for loop-free paths or loops with certain properties in the extended unification graph, according to the type of unification conflict. Algorithms for the handling of the unification graph and for the extraction of information from it are described and proved as correct.