Many different strategies have been tried for selecting the clauses to
be resolved. These include:
- level saturation or two-pointer method: the outer pointer
starts at the negated conclusion; the inner pointer starts at the first clause.
The two clauses denoted by the pointers are resolved if possible, with the
result added to the end of the list of clauses. (There may
be multiple resolvents of two clauses.) The inner pointer is incremented
to the next clause until it reaches the outer pointer; then the outer
pointer is incremented and the inner pointer is reset to the front.
The two-pointer method is a breadth-first method that will generate
many duplicate clauses.
- set of support: One clause in each resolution step must be
part of the negated conclusion or a clause derived from it. This can be
combined with the two-pointer method by putting the clauses from the
negated conclusion at the end of the list. Set-of-support keeps the proof
process focused on the theorem to be proved rather than trying to prove