Inference in First-Order Logic: Forward Chaining — Beginner-Friendly Notes

1. What It Is

Forward chaining = data-driven reasoning: start from known facts and repeatedly apply rules whose premises are satisfied to derive new facts, forward until query is derived or no new facts.

Facts + Rules → New Facts → Repeat.

2. Form Required — Horn Clauses

Forward chaining works efficiently on definite clauses: a disjunction with exactly one positive literal, written as implication:

P1 ∧ P2 ∧ ... ∧ Pn ⇒ Q   (Q is single positive literal)
Facts are like  ⇒ Q  (no premises)

Example KB:

• $Bird(Tweety)$
• $\forall x\ (Bird(x) \Rightarrow Flies(x))$ → rule $Bird(x) \Rightarrow Flies(x)$
• Query: $Flies(Tweety)$?

3. How It Works (with unification — preview)

• Match: find rule whose premises unify with known facts (e.g., $Bird(x)$ unifies with $Bird(Tweety)$ via $x/Tweety$).
• Fire: derive consequent $Flies(Tweety)$.
• Add to KB and repeat.

Trace:

KB: Bird(Tweety)
Rule: Bird(x) ⇒ Flies(x)  with {x/Tweety} ⇒ Flies(Tweety)  [derived]
Query Flies(Tweety) now true.

4. Algorithm Sketch (for exam)

repeat:
  newFacts = { Q | rule P⇒Q where P satisfied by KB via unification }
  if query in newFacts: return true
  if newFacts ⊆ KB: return false (no progress)
  KB = KB ∪ newFacts

5. Properties

Property	Value
Sound	Yes (only derives entailed facts)
Complete	Yes for definite clauses (Horn KB)
Strategy	Breadth-like, derives all consequences — good when you want all facts

6. When to Use (vs Backward)

• Use forward when many queries need many derived facts, or you want to compute closure (e.g., expert system that propagates all diagnoses).
• Analogous to BFS: explores all consequences.

7. One-Line Summary

Forward chaining repeatedly matches definite-clause rules against known facts via unification, deriving new facts data-forward until the query is entailed or fixed point is reached, and is sound and complete for Horn KBs.

8. Quick Self-Check

1. Why does forward chaining need Horn clauses to be efficient?
2. Give a fact that would not trigger $Bird(x) \Rightarrow Flies(x)$.