Binary Resolution

Binary resolution is a generalization of the following rule, which, as you may recall, we noted to be valid for the propositional calculus.

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

The generalization is achieved by letting the variables here range over literals, and by insisting that $\psi$ and $\neg \psi$ unify. This unification is applied to $\phi$ and $\chi$ as well, and they are produced in unified form as a disjunction. As an example, binary resolution could produce the third of the following clauses from the previous two.

1.

$\neg$Likes $(x,\mbox{john})$ $\vee$ Happy(x)

2.

$\neg$Happy(x) $\vee$ $\neg$Smart(x)

3.

$\neg$Likes $(x,\mbox{john})$ $\vee$ $\neg$Smart(x)

We assume that you can adapt, on your own, all the specific resolution strategies we visited in Chapter 2 so that they are based on unification rather than on contradiction. But someone may ask: What about identity? Doesn't this require entirely new mechanisms than those seen in the propositional case? Yes, identity is something special. We will discuss it by discussing two inference schemas for identity used by OTTER, namely, paramodulation and demodulation.