Hyper-resolution

The schema for hyperresolution looks like this:

$$\begin{array}{ll} \Phi_1 \cup \{\neg\psi_1, \neg\psi_2, \ldo... ...Phi_1 \cup \Phi_ 2 \cup \cdots \cup \Phi_{n+1} &\\ \end{array}$$

Now here is an example in OTTER, first an input file and then an output file showing the proof. Note here that both ur-resolution and hyper-resolution are used.

% An input file for evoking hyperresolution.

set(hyper_res).
set(ur_res).

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

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

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

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

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