Forward and Backward Chaining in FOL

Forward Chaining in FOL

Extends propositional forward chaining (Ch.7) to FOL using GMP.

Idea: start from ground facts, repeatedly apply GMP to derive new facts until query proved or no new facts can be derived.

function FOL-FC-ASK(KB, α) returns substitution or false
    repeat until new is empty
        new ← {}
        for each rule (p₁ ∧ ... ∧ pₙ → q) in KB do
            for each θ such that SUBST(θ, p₁ ∧ ... ∧ pₙ) matches facts in KB do
                q' ← SUBST(θ, q)
                if q' does not unify with any fact or goal in KB then
                    add q' to new and KB
                if q' unifies with α then return θ
        add new to KB
    return false

Pattern Matching

Finding θ such that all pᵢ match facts in KB requires conjunctive query processing — matching multiple atoms simultaneously.

Naive: for each rule with n body literals, n nested loops over KB facts. Efficient implementations use indices.

Properties

Property	Value
Sound	Yes
Complete (datalog)	Yes — if KB is function-free (Datalog)
Complete (full FOL)	Semi — may loop with functions
Terminates	Yes if function-free; may loop otherwise

Datalog: FOL restricted to no function symbols → ground terms are just constants → finite KB → forward chaining terminates.

Backward Chaining in FOL

Goal-directed, top-down. Given a query goal, find rules whose head unifies with the goal, recursively prove the body.

function FOL-BC-ASK(KB, goals, θ) returns substitution
    if goals is empty then yield θ
    q ← SUBST(θ, FIRST(goals))
    for each clause (lhs → rhs) in KB where UNIFY(rhs, q) = θ' succeeds
        θ'' ← FOL-BC-ASK(KB,
                          SUBST(θ', lhs) + REST(goals),
                          θ')
        for each θ''' in θ'' do yield θ'''

The algorithm is a generator — yields all solutions.

Prolog

Prolog is a practical implementation of FOL backward chaining: - KB = set of Horn clauses written as: head :- body. - Query = ?- goal. - Depth-first left-to-right search (not breadth-first) - Unification with occur-check disabled (for efficiency) - Extra-logical predicates: assert, retract, cut (!)

Prolog does not use the most general unifier in all cases — cut and other control flow break pure logical semantics.

Forward vs. Backward in FOL

	Forward Chaining	Backward Chaining
Direction	Facts → goal	Goal → facts
Derives	All consequences	Only what’s needed for query
Complete	Yes (Datalog)	Yes (with loop detection)
Prolog analog	Datalog	Prolog
Best when	Many conclusions needed	Specific goal

Loop Detection

Backward chaining can loop:

Ancestor(x,y) :- Parent(x,y).
Ancestor(x,y) :- Parent(x,z), Ancestor(z,y).

Query Ancestor(John, John) → may recurse forever.

Fix: maintain a visited set of goals. Don’t re-enter a goal already on the stack.

Memoization (tabling in Prolog) = cache proved/failed subgoals. This converts exponential backward chaining into polynomial in some cases — connection to dynamic programming.

Constraint Logic Programming

Extension of Prolog: variables range over constrained domains (integers, reals). Constraints propagated during search — like CSP arc consistency (Ch.6) combined with Prolog.

Used in scheduling, configuration, optimization — very practical.