Binary Resolution

Binary resolution for propositional languages is the following rule.

$$\begin{array}{c} \phi \vee \psi \quad \neg\psi \vee \chi\\ \hline \phi \vee \chi\\ \end{array}$$

Let's use OTTER to carry out a proof using this rule. Suppose that we know $P \vee Q$, $\neg Q \vee R$, and that we want to prove $P \vee R$. In order to do this we can used the denial of what it is we're aiming to show, i.e., $\neg (P \vee R)$; this denial can be converted to clausal form by distributing the negation sign in using DeMorgan's Law; this yields $\neg P \wedge \neg Q$, which can be broken out into two separate clauses. Here is the input file to OTTER (for now, do not concern yourself with the fact that the formulas in this input are divided into two sets, usable and sos):

% Activate the inferenc rule binary resolution:
set(binary_res).

list(usable).
P | Q.
end_of_list.

list(sos).
-Q | R.
-P.
-R.
end_of_list.

And here is the resultant proof, with the use of binary resolution indicated:

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

1 [] P|Q.
2 [] -Q|R.
3 [] -P.
4 [] -R.
5 [binary,3.1,1.1] Q.
6 [binary,2.1,5.1] R.
7 [binary,6.1,4.1] $F.

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