Logic 5 - Propositional Modus Ponens | Stanford CS221: AI (Autumn 2021)

Main ideas and lessons

• Goal of the module: Explain how modus ponens can be used in propositional logic to achieve both:

  • Soundness: If you can derive a statement, then it is semantically entailed by the knowledge base.
  • Completeness: If a statement is semantically entailed by the knowledge base, then you can derive it syntactically.

• Problem identified: The standard modus ponens is sound but not complete in full propositional logic.

• Fix proposed: Restrict the formulas to a special class called Horn clauses (also called “horned clauses” in the subtitles), and then show that modus ponens becomes complete with respect to those clauses.

---

Key definitions (Horn / definite / goal / “foreign” clauses)

1) Definite clause

A definite clause has the form:

[ p_1 \wedge p_2 \wedge \dots \wedge p_k \Rightarrow q ]

Where:

• (p_1, \dots, p_k) and (q) are propositional symbols
• (k) can be 0, meaning:
  • If (k=0), the antecedent is “true,” so the clause becomes: [ \text{true} \Rightarrow q ] which is equivalent to just: [ q ]

Examples (as described)

• “rain and snow imply traffic” → definite clause (positive literals in the antecedent, and a single positive literal in the consequent)

• “traffic” → definite clause (case (k=0))

Not definite clause

• “not traffic implies …” is not definite because it introduces negation in the antecedent (negation is disallowed).
• “random snow implies peaceful OR …” is not definite because the consequent must be a single positive symbol (no disjunction in the consequent).

---

2) Goal clause

A goal clause has the form:

[ p_1 \wedge p_2 \wedge \dots \wedge p_k \Rightarrow \text{false} ]

Example:

• “traffic and accident imply false” → goal clause

Interpretation:

• This is equivalent to negation of the antecedent.
• In words:
  • ((p_1 \wedge \dots \wedge p_k) \Rightarrow \text{false}) means “it cannot be that all of these hold,” expressible as a large disjunction of negations.

---

3) Horn clause (“foreign clause” in subtitles)

A Horn clause is either:

• a definite clause, or
• a goal clause.

---

Modus ponens for Horn clauses (generalized form)

The subtitles use a more general modus ponens rule.

Generalized modus ponens

Given:

• [ p_1 \wedge \dots \wedge p_k \Rightarrow q ]

• [ p_1 \wedge \dots \wedge p_k ]

Conclude:

• [ q ]

Example used in the subtitles (intuitive story):

• “It is wet and it is a weekday”
• “If it isn’t wet and it is a weekday there is traffic” (presented informally)

These combine to infer traffic using the generalized modus ponens pattern.

---

The completeness + soundness claim (restricted to Horn clauses)

Core theorem/claim

• If you apply modus ponens only on Horn clauses, then it is:
  • Sound
  • Complete (with respect to entailment)

What “completeness” means here

Assume a knowledge base (KB) containing only Horn clauses.

• If a propositional symbol (p) is entailed by KB (i.e., ( \text{KB} \vDash p )),
• then using the modus ponens derivation system you can derive it syntactically (i.e., ( \text{KB} \vdash p )).

Why this helps with “ask/tell” operations

• Semantically, checking whether KB entails (p) requires:
  • model checking / satisfiability / entailment testing (described as involved).
• With soundness + completeness under the Horn restriction, you can instead:
  • do syntactic derivations using modus ponens
  • treat derivability as equivalent to entailment.

Equivalence emphasized

In the Horn setting:

• Derivation (syntactic) ⇔ Entailment (semantic)

---

Detailed example: entailment checked via derivation

• Given: a knowledge base consisting only of Horn clauses
• Question (ask): “Is ( \text{Traffic} ) true?” Interpreted as: does KB entail Traffic?

Method

• Check whether you can derive ( \text{Traffic} ) syntactically using generalized modus ponens.
• Identify rules in KB like:
  • [ ( \text{rain} \wedge \text{weekday} ) \Rightarrow \text{traffic} ] and derive needed antecedents from other clauses.

Example sequence from the subtitles

Start with KB facts/rules like:

• rain
• rain ⇒ wet
• weekday
• (wet ∧ weekday) ⇒ traffic (a Horn clause)

Apply modus ponens:

1. From rain and rain ⇒ wet, derive wet
2. Now you have wet and weekday
3. From (wet ∧ weekday) ⇒ traffic plus wet and weekday, derive traffic

Conclusion

• Because modus ponens is sound and complete for Horn clauses:
  • if the derivation succeeds, then KB entails traffic.

---

Big picture: syntax vs. semantics

• Syntax land:
  • formulas and inference rules (derivation)
• Semantic land:
  • meanings via models
  • entailment checking corresponds to satisfiability/model checking (described as harder)

Key takeaway:

• If inference rules are sound and complete (achieved here by restricting to Horn clauses),
• then derivation becomes equivalent to entailment checking, avoiding expensive semantic checking.

---

Final note about the next topic

• The module restricts formulas to enable both soundness and completeness using modus ponens.
• The next module will use a more powerful inference method (resolution) rather than changing the formula class.

---

Speakers / sources featured

• Stanford CS221 (Autumn 2021) (course/source)
• No individual speaker name is provided in the subtitles (only “you”/instructor narration is present).