A Generalization of Resolution

This paper defines a generalization of the resolution principle for theorem-proving, which permits a hierarchical organization within the theorem-prover. The generalization corresponds to an extension of the usual unification procedures. A graph-theoretic categorization of sets of clauses with input or unit refutations is given, and completeness theorems are proved in this category. In the case of sets of clauses which include the equality predicate, the generalization gives a new technique for treating equality, for which a completeness theorem is proved. An implementation of these ideas gives results which suggest that this is a more efficient method for treating equality than previously proposed schemes. (Author)