kr - resolution logic

http://en.wikipedia.org/wiki/Resolution_(logic)

A simple example

\frac{a \vee b, \quad \neg a \vee c} {b \vee c}


In English: if a or b is true, and a is false or c is true, then either b or c is true.

If a is true, then for the second premise to hold, c must be true. If a is false, then for the first premise to hold, b must be true.

So regardless of a, if both premises hold, then b or c is true.


Claim: Resolvent is entailed by input clauses.
Suppose I |= (p ∨ α) and I |= (¬p ∨ β)
I |= p
Case 1:
then I | = β, so I |= (α ∨ β).
I |≠ p
Case 2:
then I | = α, so I | = (α ∨ β).
I | = (α ∨ β).
Either way,
{(p ∨ α), (¬p ∨ β)} |= (α ∨ β).
So: