Some theorem-proving strategies based on the resolution principle

The formulation of the resolution principle by J. A. Robinson (1965a) has provided the impetus for a number of recent efforts in automatic theoremproving. 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 or its negation F(xi, x2,.-.., x) 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. For example, the number-theoretic proposition'For all x and y, if x is a divisor of y then there exists some z such that x times z equals y' may be symbolised as D(x, y)v T(x, f(x, y), y) in which D(x, y)' stands for x is a divisor of y' and 7(x, y, z)' stands for'x times y equals z'.