Inference & Reasoning Systems

Jr Codex AI Notes

Level: Intermediate–Advanced Prerequisites: Chapter 3 Time to complete: ~30 minutes

Table of Contents

1. From Entailment to Practical Inference
2. Inference Rules
3. Forward Chaining
4. Backward Chaining
5. Forward vs Backward — When to Use Which
6. Resolution
7. Soundness & Completeness
8. Summary & Next Steps

1. From Entailment to Practical Inference

Chapter 2 defined entailment (KB ⊨ α) and checked it via brute-force model checking — enumerating every possible world. That approach is correct but scales as 2^n, utterly impractical for any real knowledge base. Inference is the process of deriving new sentences from a knowledge base using specific, efficient rules — without ever enumerating every possible world.

Model Checking (Ch.2)                  Inference (this chapter)
─────────────────────────────         ─────────────────────────────
  Enumerate EVERY possible world,        Apply specific RULES to
  check if KB→query holds in ALL           DERIVE new true sentences
  of them                                    directly, never enumerating
                                               all possible worlds

  Correct, but EXPONENTIALLY slow          Fast, IF the right rules
                                             and strategy are used
─────────────────────────────────────────

2. Inference Rules

An inference rule lets you derive a new sentence from existing ones, guaranteed to preserve truth — if the inputs are true, the output must be true too.

Modus Ponens — the Most Fundamental Rule
─────────────────────────────────────────
  Given:   P → Q     (if P then Q)
             P          (P is true)
  Derive:      Q           (therefore, Q is true)
─────────────────────────────────────────

def modus_ponens(kb, implication, antecedent):
    """
    implication: a tuple (P, Q) representing "P implies Q"
    antecedent: the fact P, which must already be in kb
    Returns Q if the rule applies, else None.
    """
    P, Q = implication
    if P in kb and antecedent == P:
        return Q      # DERIVE Q
    return None
 
kb = {"Rain"}
implication = ("Rain", "WetGround")
derived = modus_ponens(kb, implication, "Rain")
print(derived)      # "WetGround" — newly derived fact

Other Standard Inference Rules
─────────────────────────────────────────
  Modus Tollens:      P → Q, ¬Q  ⊢  ¬P
                        ("if it were P, Q would follow — but Q
                         is false, so P must be false too")

  And-Elimination:       P ∧ Q  ⊢  P   (and also  ⊢  Q)
                            ("if BOTH are true, EACH individually
                             is true")

  Unit Resolution:          P ∨ Q, ¬P  ⊢  Q
                              ("one of these is true; it's not P,
                               so it must be Q")
─────────────────────────────────────────

3. Forward Chaining

Forward chaining starts from known facts and repeatedly applies inference rules (mainly Modus Ponens) to derive new facts, continuing until no more new facts can be derived — a data-driven strategy.

def forward_chaining(facts, rules):
    """
    facts: a set of known true propositions
    rules: a list of (premises, conclusion) tuples — premises is a LIST of
           facts that, if ALL known, allow deriving conclusion
    """
    facts = set(facts)
    changed = True
 
    while changed:
        changed = False
        for premises, conclusion in rules:
            if all(p in facts for p in premises) and conclusion not in facts:
                facts.add(conclusion)
                changed = True      # keep looping — this new fact might unlock MORE rules
 
    return facts
 
rules = [
    (["Man", "Greek"], "Mortal"),        # if Man and Greek, then Mortal
    (["Mortal"], "WillDie"),                # if Mortal, then WillDie
]
initial_facts = ["Man", "Greek"]
 
all_derived_facts = forward_chaining(initial_facts, rules)
print(all_derived_facts)      # {'Man', 'Greek', 'Mortal', 'WillDie'} — chained derivation

Forward Chaining, Visualized
─────────────────────────────────────────
  Known: Man, Greek
      │
      ▼ (rule: Man ∧ Greek → Mortal)
  Derived: Mortal
      │
      ▼ (rule: Mortal → WillDie)
  Derived: WillDie
      │
      ▼ (no more rules apply — STOP)
─────────────────────────────────────────

Forward chaining keeps deriving everything possible from the facts it has — useful when you want to know "everything that follows" from a set of known facts, without a specific question in mind yet.

4. Backward Chaining

Backward chaining starts from a specific goal (a query you want to prove) and works backward, asking "what would need to be true for this to hold?" — a goal-driven strategy.

def backward_chaining(goal, facts, rules, depth=0):
    """Attempt to prove `goal` is true, given known facts and rules."""
    indent = "  " * depth
    print(f"{indent}Trying to prove: {goal}")
 
    if goal in facts:
        print(f"{indent}✓ {goal} is a known fact")
        return True
 
    for premises, conclusion in rules:
        if conclusion == goal:
            print(f"{indent}Found rule: {premises} → {goal}")
            if all(backward_chaining(p, facts, rules, depth + 1) for p in premises):
                print(f"{indent}✓ All premises for {goal} proven")
                return True
 
    print(f"{indent}✗ Cannot prove {goal}")
    return False
 
result = backward_chaining("WillDie", facts={"Man", "Greek"}, rules=rules)
print(f"\nFinal result: {result}")

Backward Chaining, Visualized
─────────────────────────────────────────
  Goal: WillDie?
      │
      ▼ (rule: Mortal → WillDie — need Mortal)
  Goal: Mortal?
      │
      ▼ (rule: Man ∧ Greek → Mortal — need BOTH)
  Goal: Man?  → YES, known fact ✓
  Goal: Greek? → YES, known fact ✓
      │
      ▼ (both premises proven — Mortal is proven)
      ▼ (Mortal proven — WillDie is proven)
  RESULT: True
─────────────────────────────────────────

Backward chaining only explores rules relevant to the specific goal — much more efficient than forward chaining when you have one specific question and a large knowledge base with many irrelevant facts/rules.

5. Forward vs Backward — When to Use Which

Decision Guide
─────────────────────────────────────────
  Want to know EVERYTHING that follows from current facts,
  no specific question yet (e.g. monitoring a system, alerting
  on any derivable dangerous condition)
      → Forward chaining (data-driven)

  Have ONE SPECIFIC question/goal, and a large knowledge base
  where MOST facts/rules are irrelevant to answering it
  (e.g. "can Tweety fly?", "is this transaction fraudulent?")
      → Backward chaining (goal-driven)
─────────────────────────────────────────

6. Resolution

Resolution is a single, powerful inference rule that (with the right setup) is both sound and complete for propositional logic — meaning it can, in principle, prove any valid entailment, unlike the more limited combination of rules used in Sections 2-4.

The Resolution Rule
─────────────────────────────────────────
  Given two clauses (sentences in OR-form) sharing a
  COMPLEMENTARY literal (P in one, ¬P in the other):

    (P ∨ Q)   and   (¬P ∨ R)
  ────────────────────────────
             (Q ∨ R)

  The complementary P/¬P pair CANCELS OUT, and everything
  else combines into a new clause.
─────────────────────────────────────────

def resolve(clause1, clause2):
    """
    clause1, clause2: sets of literals (strings; a leading '¬' means negation)
    Returns the resolvent clause if a complementary pair is found, else None.
    """
    for literal in clause1:
        negation = literal[1:] if literal.startswith("¬") else "¬" + literal
        if negation in clause2:
            resolvent = (clause1 - {literal}) | (clause2 - {negation})
            return resolvent
    return None
 
clause1 = {"P", "Q"}          # P ∨ Q
clause2 = {"¬P", "R"}           # ¬P ∨ R
result = resolve(clause1, clause2)
print(result)      # {'Q', 'R'} — Q ∨ R

Proof by Resolution (Refutation) — the Standard Strategy
─────────────────────────────────────────
  To prove KB ⊨ α:
    1. Convert KB AND the NEGATION of α into clause form
    2. Repeatedly apply resolution to pairs of clauses
    3. If this process ever derives the EMPTY clause (a
       contradiction), the ORIGINAL assumption (¬α) must
       be false — meaning α IS entailed by KB

  This is "proof by contradiction": assume the OPPOSITE
  of what you want to prove, show it leads to an
  impossibility, conclude the original claim must hold.
─────────────────────────────────────────

Resolution is the foundational technique behind Prolog and many automated theorem provers — a single, uniform rule (rather than needing many special-case rules like Modus Ponens, Modus Tollens, etc.) that's provably complete for propositional logic.

7. Soundness & Completeness

Two formal properties every inference system should be evaluated against — directly extending Chapter 2's rigor to the algorithms in this chapter:

Soundness
─────────────────────────────────────────
  An inference algorithm is SOUND if it only derives
  sentences that are ACTUALLY entailed — it never produces
  a FALSE conclusion from true premises.

  (Every rule in Section 2, used correctly, is sound.)
─────────────────────────────────────────

Completeness
─────────────────────────────────────────
  An inference algorithm is COMPLETE if it can derive
  EVERY sentence that IS entailed — it never "misses" a
  valid conclusion.

  Forward/backward chaining (Sections 3-4) are complete
  ONLY for a restricted class of rules (definite clauses,
  like the examples used above) — NOT for general logic.

  Resolution (Section 6) IS complete for full propositional
  logic — this is precisely why it's the standard technique
  for general-purpose automated theorem proving.
─────────────────────────────────────────

Why this distinction matters practically: a sound-but-incomplete system (like basic forward/backward chaining on non-definite-clause rules) might simply fail to find a valid proof that exists — not because the proof is wrong, but because the algorithm's search strategy can't reach it. Resolution's completeness guarantee is what makes it the tool of choice when correctness must be airtight.

8. Summary & Next Steps

Key Takeaways

• Inference derives new sentences from a knowledge base using specific rules (Modus Ponens, resolution, etc.), avoiding the exponential cost of Chapter 2's brute-force model checking.
• Forward chaining is data-driven, deriving everything possible from known facts; backward chaining is goal-driven, working backward from a specific query — pick based on whether you have a specific question or want exhaustive derivation.
• Resolution is a single, uniform inference rule that's both sound and complete for propositional logic, forming the basis of Prolog and automated theorem provers.
• Soundness means an algorithm never derives false conclusions; completeness means it can derive every true entailment — resolution achieves both for propositional logic, while simple chaining is complete only for restricted rule forms.

Concept Check

1. Why is inference generally faster than the brute-force model checking from Chapter 2?
2. When would backward chaining be more efficient than forward chaining, and why?
3. What does it mean for resolution to be "complete," and why does that matter for automated theorem proving?

Next Chapter

→ Chapter 5: Automated Planning

Jr Codex — 1-on-1 Personalized Coaching | Back to Module Index