The Resolution Rule (Propositional Case)

The resolution inference rule, for the propositional case, is now easy to state in set-theoretic terms. Let $\Phi$ and $\Psi$ be sets of clauses. Then

$$\begin{array}{ll} \Phi & \mbox{with } \phi \in \Phi\\ \Psi ... ... (\Phi - \{\phi\}) \cup (\Psi - \{\neg \phi\}) &\\ \end{array}$$

For an example of this rule in action, consider the following proof, which takes as a starting point the four clauses produced in our fourth example of conversion to clausal form just above. Note that at line 6 we reach the empty clause; this is how a contradiction is represented in resolution-based reasoning. (The contradiction here shows that $((P \rightarrow Q) \wedge \neg Q) \rightarrow \neg P$ is a theorem of the propositional language $\cal L$$_{PC}^\infty$, since the contradiction is produce by negating this formula.)

$$\begin{array}{lll} 1 & \{\neg P, Q\} & \mbox{given}\\ 2 & \... ...given}\\ 5 & \{\neg P\} & 1,3\\ 6 & \{\} & 4,5\\ \end{array}$$