UR-Resolution

UR-resolution applies to a set of clauses, one of which must be a non-unit clause, the others of which must be unit clauses; the result is a unit clause. The non-unit clause must contain exactly one more clause than there are unit clauses in the premises. Here is the schema:^3.2

$$\begin{array}{ll} \phi_1 \vee \phi_2 \vee \cdots \vee \phi_n... ... \ldots, \phi^{n-1}_k\} & \mbox{(a unit clause)}\\ \end{array}$$

Here, using OTTER, is an example. We show the input file first, then the output file containing the proof. Notice that binary resolution is also used in this example.

% Example showing UR-resolution in action.

% Turn ur-resolution on:
set(ur_res).

list(usable).
p | q | -r | s.
end_of_list.

list(sos).
-q.
r.
-s.
-p.
end_of_list.

---------------- PROOF ----------------

1 [] p|q| -r|s.
2 [] -q.
3 [] r.
4 [] -s.
5 [] -p.
6 [ur,4,1,2,3] p.
7 [binary,6.1,5.1] $F.

------------ end of proof -------------