SOME THEOREM-PROVING STRATEGIES BASED ON THE RESOLUTION PRINCIPLE JARED L. DARLINGTON

The formulation of the resolution principle by J. A. Robinson (1965a) has provided the impetus for a number of recent efforts in automatic theoremproving. In particular, the program PG1 (Wos et al. 1964, 1965), written by L. Wos, G. A. Robinson and D. F. Carson for the Control Data 3600, utilises the resolution principle in conjunction with a'unit preference strategy' and a'set of support strategy' to produce efficient proofs in first-order functional logic and group theory. These programs have generated proofs of some interesting propositions of number theory, in addition to theorems of first-order functional logic and group theory. A'literal' is an n-place predicate expression F(xi, x2,.-.., x) or its negation F(xi, x2,., x „) whose arguments are individual variables, individual constants, or functional expressions. Quantifiers do not occur in these formulae, since existentially quantified variables have been replaced by functions of universally quantified ones, and the remaining variables may therefore be taken as universally quantified.