Doing a Resolution Proof

What is the problem

You’ll be given:

• a bunch of premises.
• a conclusion.

and asked to prove that the conclusion is implied by the premises.

TL;DR

We’ll do it by proving that the premises can’t be true while the conclusion is false; adding the negated conclusion to the set of premises leads to a contradiction.

---

We’ll work in 2 phases,

1. first convert all the premises into CNF, along with the conclusion (and also negating it).
2. do the resolution proof using these premises + negated conclusion.

Before you begin

1. …

Strategy

Phase 1 (conversion to CNF)

…

Phase 2 (the proof)

1. combine pairs of clauses into a new one via resolution until u reach a contradiction.

Make sure to...

Make sure to always begin by combining the negated conclusion clause with another one, since this is what u know will begin the contradiction.

• add the new clause as a line containing the following:
  1. the index of the clause.
  2. the clauses that formed it, place the clause of a smaller size to the left of the other one.
  3. the resulting clause after resolution.
• here’s what happens when we keep pairing clauses (we eventually reach a contradiction)
  

---

Connections