Logic 4 - Inference Rules | Stanford CS221: AI (Autumn 2021)

Main ideas / concepts

• Inference rules connect the syntax of formulas to reasoning about what follows from a knowledge base.
• The lecture distinguishes two “lands”:
  • Syntax land: formulas are manipulated by symbolic rules (inference rules). Inference rules apply to form, not meaning.
  • Semantic land: each formula has a set of models (assignments/worlds where it is true). Truth is about models and entailment.
• A knowledge base (KB) is a set of formulas.
  • The KB has a corresponding set of models (those worlds satisfying all formulas in the KB).

Goal of inference

From formulas in the KB, infer a new formula g such that the models of g are appropriately related to the models of the KB. The desired relationship is:

• KB entails g ⇔ models(KB) ⊆ models(g)
  • (Equivalently: g is true in every model of KB.)

---

Example to build intuition

Given:

• “It is raining.” (fact)
• “If it is raining then it is wet.” (rule)

Inference should let you conclude:

• “Therefore it is wet.”

This is the classic role of modus ponens.

---

Modus ponens (specific inference rule)

Form

• Premises:
  • p
  • p ⇒ q
• Conclusion:
  • q

Key property emphasized later

• Modus ponens is sound but not complete (with respect to entailment in full propositional logic).

---

General form of an inference rule

An inference rule can be represented as:

• Premises: f₁, f₂, …, f_k
• Conclusion: g

The rule allows you to derive g by syntactically matching and manipulating formulas in the knowledge base.

---

Inference algorithm (procedural methodology)

The lecture describes an inference algorithm as a loop that repeatedly applies inference rules to add new information.

Algorithm structure (as described)

• Input: a knowledge base (set of formulas) and a set of inference rules (e.g., modus ponens)
• Repeat:
  • Select a subset of formulas from the current KB
  • If the selected formulas match the premises pattern of some inference rule:
    • Use the inference rule to infer a new formula g
    • Add g to the knowledge base
• Stop when:
  • There are no changes / no new formulas can be added

This process continues until the knowledge base reaches a fixed point (no further derivations are possible).

---

Derivation / proving (syntactic notion)

• A knowledge base derives (or proves) a formula f if:
  • f eventually gets added to the knowledge base through the inference algorithm.

Notation discussed:

• KB derives/proves f when f appears through repeated rule application.

---

Entailment vs derivation (semantic vs syntactic)

• Entailment (semantic):
  • KB entails f when f is true in all models of KB, i.e.:
    • models(KB) ⊆ models(f)
• Derivation (syntactic):
  • KB derives f when the inference algorithm can produce f by rule application.

The lecture asks how these relate and introduces:

---

Soundness and completeness (bridge between entailment and derivation)

Soundness

• Idea: anything you derive should be true.

• Conceptual formalization:

  • If KB derives f, then KB must entail f.

• “Glass” metaphor:

  • Truth/entailed formulas are “inside the glass.”
  • A sound inference system never derives anything “outside the glass” (never false).

Completeness

• Idea: everything that is true (entailed) should be derivable.

• Conceptual formalization:

  • If KB entails f, then KB must be able to derive f.

• Completeness fills “the whole glass” (no true formula left undeduced).

Combined effect

• If you have sound + complete, then:
  • derivation and entailment become equivalent.

Practical emphasis

• In practice, soundness is prioritized:
  • deriving falsehoods is unacceptable
  • completeness may be harder, so approximation may be tolerated

---

Worked derivation example (modus ponens only)

KB contains:

1. “It is raining.”
2. “If raining then wet.”
3. “If wet then slippery.”

Using modus ponens repeatedly:

• From (1) and (2) ⇒ derive wet
• From (derived wet) and (3) ⇒ derive slippery

At fixed point:

• no further formulas can be derived using only modus ponens.

The lecture also notes:

• You may derive some truths and not others if the inference system lacks completeness.

---

Checking soundness (model-based method)

To test an inference rule’s soundness, the lecture describes a semantic check using models:

For a rule like: if p and (p ⇒ q), conclude q:

• Consider models(p) and models(p ⇒ q)
• Their intersection corresponds to where both premises hold
• Verify that this intersection is a subset of models(q)
• If always true ⇒ the rule is sound

---

Modus ponens: sound but not complete

Soundness of modus ponens

• The lecture concludes modus ponens is sound because the required model inclusion holds.

Incompleteness evidence

• Example scenario:
  • KB contains rain implies slippery, but modus ponens alone might not derive rain ⇒ slippery (or other entailed forms) when the necessary syntactic structure doesn’t match modus ponens’ required pattern.

Core reason given:

• Modus ponens only applies when you can match the specific syntactic form:
  • f and (f ⇒ g)
• It does not naturally handle logical structures like disjunction (OR) in the same way.

---

How to fix the incompleteness (two options)

The lecture proposes two main strategies:

1. Restrict the logic to a smaller class

   • Restrict propositional formulas to Horn clauses
   • Under this restriction:
     • modus ponens becomes sound and complete

2. Use more powerful inference rules

   • Keep full propositional logic, but strengthen the inference mechanism
   • Introduce resolution later:
     • resolution is stated to be sound and complete

The lecture says the next modules will cover:

• Horn clauses / restriction approach (where modus ponens achieves completeness)
• Resolution (where a stronger rule system achieves completeness without restricting logic)

---

Speakers / sources featured

• Stanford CS221 (Autumn 2021) — course/source of the lecture content (explicitly referenced by the video title).
• No individual speaker name is provided in the subtitles.