No abstract available.

This paper develops a method of mechanical deduction based on a graphical representation of the structure of proofs. Attempts to find a refutation(s) are recorded in the form of plans, corresponding to portions of an AND/OR graph search space and representing a purely deductive structure of derivation. This method can be applied to any initial base (set of nonnecessarily Horn clauses). Unlike the exhaustive (blind) backtracking which treats all the goals deduced in the course of a proof as equally probable sources of failure, his approach detects the exact source of failure. Only a small fragment of the solution space is kept on disk as a collection of pairs, each of which consists of a plan and a graph of constraints. The search strategy and the method of nonredundant processing of individual pairs which leads to a solution (if it exists) is presented. This approach is compared¿on a special case¿with a blind backtracking algorithm for which an exponential improvement is demonstrated. Some important implementation problems are discussed, and toplevel design of a mechanical deduction system implementing our algorithm is presented. It is proven that the algorithm is complete in the following sense: if for a given base a resolution refutation exists, then this refutation is found by the algorithm.

A proof procedure is described that relies on the construction of certain directed graphs called ``deduction plans.'' Plans represent the structure of proofs in such a way that problem reduction may be used without imposing any ordering on the solution of subproblems, as required by other systems. The structure also allows access to all clauses deduced in the course of a proof, which may then be used as lemmas. Economy of representation is the maximum attainable, consistent with this unrestricted availability of lemmas. Restricted versions of this deduction system correspond to existing linear deduction procedures, but do not suffer from some of their shortcomings, such as redundant representation, strict ordering of subproblems, and explicit substitution. One of the rules for constructing plans, however, allows a subproblem to be factored to a previously solved one: this has no equivalent in existing system. A further economy is obtained by making it unnecessary to perform substitutions and calculate most general unifiers. The source of unification failure can be located when a subproblem is found to be unsolvable, so that exact backtracking can be performed rather than the blind backtracking performed by existing systems. Therefore, a deduction system based on the construction of plans can avoid the wasteful search of irrelevant areas of the search space that results from the usual backtracking methods.

A generalization of the resolution method for higher order logic is presented. The languages acceptable for the method are phrased in a theory of types of order w (all finite types)—including the λ-operator, propositional functors, and quantifiers. The resolution method is, of course, a machine-oriented theorem search procedure based on refutation. In order to make this method suitable for higher order logic, it was necessary to overcome two sorts of difficulties. The first is that the unifying substitution procedure—an essential feature of the classic first-order resolution—must be generalized (it is noted that for the higher order unification the proper notion of substitution will include λ-normalization). A general unification algorithm is produced and proved to be complete for second-order languages. The second difficulty arises because in higher order languages, semantic intent is essentially more “interwoven” in formulas than in first-order languages. Whereas quantifiers could be eliminated immediately in first-order resolution, their elimination must be deferred in the higher order case. The generalized resolution procedure which the author produces thus incorporates quantifier elimination along with the familiar features of unification and tautological reduction. It is established that the author's generalized resolution procedure is complete with respect to a natural notion of validity based on Henkin's general validity for type theory. Finally, there are presented examples of the application of the method to number theory and set theory.