Resolution

Natural systems are intended to be useful for humans. There are other ways to specify a proof theory -- ways, for example, that are generally thought to be more appropriate for machines than humans. One such way is through the resolution inference rule, the core idea of which is that that if we know $P \vee Q$, and know $\neg P \vee R$, we can infer to $Q \vee R$. In this section we specify this rule for propositional languages. Our first step is furnish a procedure for converting propositional formulas to sets of clauses.