Logic 6 - Propositional Resolutions | Stanford CS221: AI (Autumn 2021)

Main ideas / concepts

• Goal of inference rules in propositional logic

  • We want inference/derivation rules that let us manipulate formula syntax to prove new formulas.
  • Key properties:
    • Correctness: only derive formulas that are logically entailed (true in all models consistent with the knowledge base).
    • Completeness: derive all formulas that are logically entailed.

• Modus Ponens (limited expressiveness)

  • Using modus ponens alone gives:
    • Correctness but not completeness (there are entailed consequences you still cannot derive using only modus ponens).

• Horn disjunct restriction as a complete fragment

  • One fix is to restrict attention to a subset of propositional logic:
    • the logic containing only Horn disjuncts.
  • In this restricted setting, applying modus ponens achieves both correctness and completeness.

• Resolution to regain completeness for full propositional logic

  • When you want to handle all of propositional logic, you use a more powerful inference rule: resolution.
  • Resolution is presented as a way to obtain correctness and completeness over general disjunctions.

---

Key logical transformations and definitions

Equivalences used (to rewrite formulas)

The instructor motivates rewriting everything using disjunctions and conjunctions:

• (P \Rightarrow Q) is equivalent to (\lnot P \lor Q).
• De Morgan’s law provides equivalences of the form:
  • Negation of a conjunction becomes a disjunction of negations.
  • Negation of a disjunction becomes a conjunction of negations.

The point is to use these equivalences so resolution can be applied in a suitable normal form.

Literals, disjuncts, Horn disjuncts

• Literal

  • A propositional symbol (P) or its negation (\lnot P).

• Disjunct

  • An OR of multiple literals, e.g. (P_1 \lor \lnot P_2 \lor P_3).

• Horn disjunct

  • A disjunct with at most one positive literal (all others, if any, are negative).
  • Example (not Horn): contains two positive literals (e.g., (P_1 \lor P_3 \lor \dots)).
  • Example (Horn): (P_1 \lor \lnot P_2 \lor \lnot P_3) (only one positive literal: (P_1)).

---

Resolution rule (concept + general form)

• Why rewrite modus ponens using disjuncts

  • The instructor notes modus ponens can be re-expressed in disjunct form as cancellation of complementary literals (a positive literal with its negation), yielding the remaining conclusion.

• Resolution intuition

  • If you have two disjunctions where one contains a literal (P) and the other contains (\lnot P), you can produce a new disjunction that removes both (P) and (\lnot P).

• Generic template described

  • If you have:
    • Disjunction #1: ((F_1 \lor \dots \lor F_n \lor P))
    • Disjunction #2: ((\lnot P \lor G_1 \lor \dots \lor G_m))
  • Then resolution derives:
    • ((F_1 \lor \dots \lor F_n \lor G_1 \lor \dots \lor G_m))

• Illustrative example

  • Knowledge about weather:
    • “rain or snow”
    • “no snow or traffic jam”
  • By treating “snow” and “not snow” as complementary, resolution yields:
    • “rain or traffic jam”

---

Correctness of resolution (models-based check)

To verify that resolution is correct, you check semantic entailment using models:

• The knowledge base restricts which truth assignments (“models”) are possible.
• For a correct derivation, the models of the knowledge base must be a subset of the models of the newly derived formula.
• In the rain/snow example, the instructor argues (via shaded regions / intersections) that this subset condition holds, so resolution is correct.

---

Conjunctive Normal Form (CNF): why resolution requires it

• Claim

  • Resolution “only works with disjuncts,” but that’s sufficient because any propositional formula can be converted to CNF.

• CNF definition

  • Conjunctive normal form = a conjunction of disjuncts.
  • Equivalently:
    • A knowledge base can be seen as a conjunction of formulas,
    • and each formula can be rewritten so it becomes a conjunction of disjuncts.

---

Detailed CNF conversion methodology (step-by-step recipe)

To convert an arbitrary propositional logic formula into CNF:

1. Eliminate implications

   • Replace each implication (A \Rightarrow B) with (\lnot A \lor B).

2. Rewrite equivalences and standardize structure

   • Use equivalences to express things using AND/OR/NOT (no implication/equivalence operators remain).

3. Push negations inward

   • Use De Morgan’s law to move NOTs inward until negations apply directly to propositional symbols (or an appropriate atomic level).

4. Remove double negations

   • Replace (\lnot\lnot X) with (X).

5. Distribute OR over AND

   • If the expression contains a disjunction of conjunctions, distribute: [ (\cdots \lor (A \land B)) \equiv ((\cdots \lor A) \land (\cdots \lor B)) ]

6. Result

   • The formula becomes a conjunction of disjuncts, i.e. CNF.

7. Model preservation

   • The instructor states that conversion to CNF preserves the set of models (same truth assignments) as the original formula.

---

Resolution-based entailment algorithm (how to check if KB ⊨ C)

Core idea

• To check whether a formula (C) is entailed by a knowledge base (KB):
  • Instead of directly testing KB ⊨ C,
  • test whether adding (\lnot C) makes the knowledge base unsatisfiable (in the method described, this corresponds to deriving an error/contradiction).

Detailed procedure

• Input

  • Knowledge base KB (a set of formulas)
  • Query formula (C)

• Steps

  • Add the negation of the query:
    • Form (KB’ = KB \cup {\lnot C}).
  • Convert every formula in (KB’) into CNF using the recipe above.
  • While possible, repeatedly apply the resolution rule to generate new disjunctions:
    • Look for complementary literals (P) and (\lnot P) across disjuncts/premises.
    • Resolve them to produce a new disjunction with those literals removed.
  • Continue resolution until:
    • A contradiction is derived (the instructor refers to an “error” outcome), or
    • resolution can no longer proceed without producing new information.

• Decision

  • If resolution derives error/contradiction:
    • conclude KB ⊨ C (i.e., KB logically follows from (C)).
  • If no contradiction is derived (per the described convergence behavior):
    • do not conclude entailment (the method would not confirm KB ⊨ C in that run).

Example structure described

• From CNF clauses such as:
  • (A)
  • ((\lnot A \lor B \lor C))
• Resolution yields:
  • ((B \lor C))
• Then, with a clause like (B):
  • Resolution can yield (C)
  • If (\lnot C) was already included initially, you can derive contradiction (“error”).

---

Time complexity discussion (why resolution is hard)

• Modus ponens (Horn setting)

  • Instructor characterizes it as relatively efficient:
    • At each step it effectively adds at most one propositional symbol.
    • With (n) symbols, it’s treated as linear-time behavior in their explanation.
  • Converges quickly because there are fewer things to consider.

• Resolution (general propositional logic)

  • In the worst case, resolution may generate many combinations of disjunctions.
  • The instructor states the worst-case behavior is exponential time.

• Reasoning complexity link

  • The procedure is framed as solving a feasibility / model checking type problem.
  • This is described as NP-complete, making exponential-time worst-case behavior unsurprising.

• Practical tradeoff

  • Use modus ponens when knowledge is representable with Horn disjuncts (faster, less expressive).
  • Use resolution for full propositional expressiveness, accepting exponential-time costs.

---

Speakers / sources featured

• Stanford CS221 (Autumn 2021) course lecture video (titled: “Logic 6 - Propositional Resolutions | Stanford CS221: AI (Autumn 2021)”).
• No individual speaker name is explicitly provided in the subtitles excerpt.