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 everything.

Contents    Page-10    Prev    Next    Page+10    Index