Resolution Principle

Definition

The resolution principle is an inference rule for clauses.

It uses a pair of opposite literals:

P
NOT P

to combine two clauses into a new clause.

Basic pattern:

(P OR A)
(NOT P OR B)
Therefore (A OR B)

Resolution eliminates a symbol and its negation across two clauses.

---

Simple Example

Clauses:

P OR Q
NOT P OR R

Resolution removes:

P
NOT P

Result:

Q OR R

The new clause contains what remains after the opposing pair is removed.

Resolution combines clauses through a shared conflict.

---

Why This Works

Consider:

P OR Q

If P is false, then Q must be true for the clause to hold.

Consider:

NOT P OR R

If P is true, then R must be true for the clause to hold.

Either way, at least one of:

Q OR R

must hold.

Resolution keeps what must remain after the opposing cases are considered.

---

Resolution And CNF

Resolution is usually applied to expressions in conjunctive normal form.

Example CNF:

(P OR Q) AND (NOT P OR R)

The clauses are:

P OR Q
NOT P OR R

Resolution produces:

Q OR R

CNF gives resolution a clean clause structure to operate on.

---

Resolution As Inference

Resolution is an inference rule.

It does not guess.

It transforms given clauses into a clause that follows from them.

Pattern:

premise clauses -> resolution rule -> new clause

This fits the broader idea:

premises -> inference -> conclusion

Resolution is one formal way to derive conclusions.

---

Final Summary

• Resolution is an inference rule for clauses.
• It uses opposite literals such as P and NOT P.
• From (P OR A) and (NOT P OR B), it derives (A OR B).
• Resolution works naturally with CNF.
• Resolution is rule-governed inference, not guessing.
• It is useful because it gives a mechanical way to derive consequences from logical clauses.