Set of Support Resolution

At this point, if you have looked carefully at the OTTER input files shown above, you may be somewhat curious. Why are the input formulas divided into two groups, one starting with list(usable), the other with list(sos)? The reason is that OTTER generally uses set of support resolution.

We say OTTER generally uses the sos strategy. You can have OTTER take an input file that contains just one group of formulas in standard first-order logic; the mode in this case is called autonomous, and is ensured with the command set(auto). Here is an example of a (very) simple proof of

$$\{P \rightarrow Q, Q \rightarrow R, \neg R \vee S, P\} \vdash S$$

in the propositional calculus using autonomous mode:

set(auto).

formula_list(usable).
p->q.
q->r.
-r|s.
p.
-s.
end_of_list.

-------> usable clausifies to:

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

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

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

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

Formally speaking, what does sos-resolution amount to? Here are the definitions. A subset $\Gamma$ of $\Delta$ is a set of support for $\Delta$ iff $\Delta - \Gamma$ is satisfiable. Given such a $\Delta$ and $\Gamma$, a set of support resolvent is a clause having at least one parent from $\Delta$ or from a descendant of $\Gamma$. A set of support deduction is one in which each derived clause is a set of support resolvent. A set of support refutation is a set of support deduction of the empty clause {}. You should at this point look back a bit to verify that the sample proofs we gave to display binary and ur-resolution were set of support refutations.