The unit preference strategy in theorem proving
L. Wos, Daniel F. Carson, George A. Robinson · 1964
Unit Preference and Set of Support Strategies The theorems, axioms, etc., to which the algorithm and strategies described in this paper are applied are stated in a normal form defined as follows: A literal is formed by prefixing a predicate letter to an appropriate number of arguments (constants, variables, or expressions formed with the aid of function symbols) and then perhaps writing a negation sign (-) before the predicate letter. For example: P(b, x) -P(b, x) Q(y) R(a, b, x, z, c) S are all literals if P, Q, R, and S are two-, one-, five-, and zero-place predicate letters, respectively. The predicate letter is usually thought of as standing for some n-place relation. Then the literal P(a, b), for example, is thought of as saying that the ordered pair (a, b) has the property P. The literal -P(a, b) is thought of as saying that (a, b) does not have the property P.