Horn Clauses, Forward Chaining, and Backward Chaining

Horn Clauses and Definite Clauses

Definite Clause

A definite clause has exactly one positive literal:

(¬l₁ ∨ ¬l₂ ∨ ... ∨ ¬lₖ ∨ m)

Written as an implication: (l₁ ∧ l₂ ∧ ... ∧ lₖ) → m

Body: l₁, ..., lₖ (premises)
Head: m (conclusion)
k=0: a fact (head unconditionally true)

Horn Clause

A Horn clause has at most one positive literal: - Definite clause (exactly one positive): A ∧ B → C - Goal clause (zero positive): A ∧ B → False

Why Horn Clauses Matter

Inference is O(n) linear time (vs. exponential for general resolution)
Many real-world KBs are Horn-expressible (rules of the form “if conditions, then conclusion”)
Basis for Prolog (backward chaining over Horn clauses)

Limitation: Not all sentences are Horn. A ∨ B (no negative literal) is not Horn.

Forward Chaining (Data-Driven)

Intuition

Start from known facts. Repeatedly fire rules whose bodies are fully satisfied. Add rule heads to KB. Repeat until query proved or no new facts derivable.

PL-FC-ENTAILS? Algorithm

function PL-FC-ENTAILS?(KB, q) returns true or false
    count    ← table: count[c] = number of body literals in c not yet proved
    inferred ← table: inferred[s] = false for all symbols s
    agenda   ← list of symbols known true (facts in KB)

    while agenda is not empty do
        p ← POP(agenda)
        if p = q then return true
        if inferred[p] = false then
            inferred[p] ← true
            for each clause c whose body contains p do
                decrement count[c]
                if count[c] = 0 then
                    add HEAD(c) to agenda
    return false

Worked Example

KB: {P, Q, P∧Q→R, Q∧R→S, R∧S→T}, query: T?

Agenda	Action
{P, Q}	Pop P → count[P∧Q→R] = 1
{Q}	Pop Q → count[P∧Q→R] = 0 → add R
{R}	Pop R → count[Q∧R→S] = 0 → add S
{S}	Pop S → count[R∧S→T] = 0 → add T
{T}	Pop T = q → return true ✓

Properties

Property	Value
Sound	Yes
Complete (Horn KBs)	Yes
Time complexity	O(n) — each symbol processed at most once

Backward Chaining (Goal-Directed)

Intuition

Start from the goal. Find rules whose head matches. Recursively prove the rule’s body. Work backward from goal toward facts.

Algorithm

function BC-OR(KB, goal, visited) returns true or false
    if goal is a known fact in KB then return true
    if goal in visited then return false      -- avoid cycles
    for each clause c in KB with HEAD(c) = goal do
        if BC-AND(KB, BODY(c), visited ∪ {goal}) then return true
    return false

function BC-AND(KB, goals, visited) returns true or false
    if goals is empty then return true
    return BC-OR(KB, FIRST(goals), visited)
        AND BC-AND(KB, REST(goals), visited)

Forward vs. Backward Comparison

Property	Forward Chaining	Backward Chaining
Direction	Facts → Goal	Goal → Facts
Style	Bottom-up	Top-down
When to use	All conclusions needed	Specific goal to prove
Redundant work	Derives irrelevant facts	May recheck same subgoal
Prolog analog	Datalog	Prolog
Fix for redundancy	—	Memoization (tabling)

Memoization in backward chaining = caching proved/failed subgoals = connection to dynamic programming.

Connection to Wumpus World

Rules like B_1_1 ∧ ¬P_2_1 → P_1_2 are Horn clauses. The agent can: - Forward chain from known percepts → derive all reachable safety conclusions - Backward chain from “Is [2,2] safe?” → trace back to needed facts

Summary

Horn clause inference via forward/backward chaining is the practically tractable core of propositional reasoning. The agenda-based propagation in PL-FC-ENTAILS? reappears in belief propagation, constraint propagation (AC-3), and distributed message-passing systems — a unifying algorithmic structure across AI.