Inference in Propositional Logic: Resolution — Beginner-Friendly Notes

1. What Inference Means

Given a knowledge base $KB$ (set of sentences believed true), entailment $KB \models α$ asks "does $α$ logically follow?" Inference is an algorithm to compute it. Resolution is a complete inference procedure for propositional logic.

2. Key Logical Equivalences (needed for CNF)

• $P \Rightarrow Q \equiv
  eg P \lor Q$
• $
  eg(P \land Q) \equiv
  eg P \lor
  eg Q$ (De Morgan)
• $
  eg(P \lor Q) \equiv
  eg P \land
  eg Q$
• Double negation: $
  eg
  eg P \equiv P$
• Distributivity: $P \lor (Q \land R) \equiv (P \lor Q) \land (P \lor R)$

3. CNF — Conjunctive Normal Form

Resolution works on CNF: a conjunction (AND) of clauses, each clause is a disjunction (OR) of literals (atoms or negated atoms).

Example CNF: $(P \lor Q) \land (
eg P \lor R) \land (
eg Q \lor
eg R)$

Steps to CNF:

1. Eliminate $\Rightarrow, \Leftrightarrow$ (use $
   eg P \lor Q$).
2. Move $
   eg$ inward (De Morgan).
3. Distribute $\lor$ over $\land$.

4. Resolution Rule (one line)

From $(C \lor P)$ and $(D \lor
eg P)$, infer$(C \lor D)$— complementary literal$P$ cancels.

(P ∨ Q) , (¬P ∨ R)  ⊢  (Q ∨ R)

5. Refutation (Proof by Contradiction) Procedure

To prove $KB \models α$:

1. Convert $KB \land
   eg α$ to CNF.
2. Repeatedly apply resolution to generate new clauses.
3. If you derive empty clause ($□$, contradiction), then $KB \models α$ is proved (since $KB \land
   eg α$ is unsatisfiable).
4. If no new clauses and no $□$ → $KB
   ot\models α$.

Tiny example:

• $KB = \{P, P \Rightarrow Q\}$ → CNF: ${P,
  eg P \lor Q}$; want$Q$.
• Add $
  eg Q$→ clauses:${P}, {
  eg P \lor Q}, {
  eg Q}$.
• Resolve $P$ with $
  eg P \lor Q$→$Q$; resolve$Q$with$
  eg Q$→$□$ → proved.

6. Why Resolution Matters

• Sound: only derives entailed sentences.
• Complete: can prove any $KB \models α$ (with refutation).
• Basis for many SAT solvers and for first-order resolution later.

7. One-Line Summary

Propositional resolution converts $KB \land
eg α$to CNF and repeatedly cancels complementary literals to derive the empty clause, providing a sound and complete refutation proof that$KB \models α$.

8. Quick Self-Check

1. Convert $P \Rightarrow Q$ to CNF.
2. Resolve $(P \lor Q)$ with $(
   eg P \lor
   eg Q)$ — what do you get?