Forward, Backward and Resolution

1Definite clauses

A definite clause has exactly one positive atom, implied by a (possibly empty) conjunction of atoms: (P_1 \wedge \cdots \wedge P_n) \rightarrow Q. In campus clothes: \mathrm{Student}(x) \rightarrow \mathrm{Person}(x), and (\mathrm{Person}(x) \wedge \mathrm{Borrowed}(x, y)) \rightarrow \mathrm{Responsible}(x, y). A fact is the n = 0 case: \mathrm{Student}(\mathrm{Priya}) is a definite clause with an empty body.

The one-positive-atom restriction is what lets a chainer treat Q as 'the thing this rule concludes' and the P_i as 'the things it needs'. A sentence with two conclusions, or a bare negation, is still first-order logic — it is just not a definite clause, and the two chainers in this lesson will not fire it. Resolution, later, drops the restriction.

2Forward chaining

Forward chaining is data-driven. Start with the facts. Whenever a rule's premises all unify with known atoms, add the head (after applying the unifier) as a new fact. Repeat until a pass adds nothing. The library KB starts with Student(Priya) and Borrowed(Priya, Dune). The first rule fires and adds Person(Priya). The second rule then fires and adds Responsible(Priya, Dune). A third pass finds nothing new, and the procedure stops.

The procedure is sound: every added atom is entailed. On a finite set of definite clauses with no function symbols it also terminates, because only finitely many ground atoms can appear. Functions reopen an infinite term world — advisor(advisor(Priya)) and so on — and a careless forward chainer can run forever even when the query is already sitting in the KB. That is a design constraint, not a footnote.

Forward loop

1. MatchFind a rule whose every premise unifies with a known fact.
2. AddApply the unifier to the head and insert that atom, if it is new.
3. RepeatStop when a full pass adds nothing — or when a asked query appears.

3Backward chaining

Backward chaining is goal-driven. Start with a query atom. If it unifies with a fact, you are done. Otherwise, find a rule whose head unifies with the query, and replace the query by that rule's premises — new subgoals. The library query Responsible(Priya, Dune) does not match a fact, so the second rule opens two subgoals: Person(Priya) and Borrowed(Priya, Dune). The second is a fact. The first is not, so the first rule opens Student(Priya), which is a fact. The query succeeds.

Nothing about Person(Omar) is ever derived, because no subgoal asked for it. That is the point on a large KB: backward chaining touches only the rules that could support this query. The cost is recursion and branching — two rules with the same head mean two alternative proofs, and a recursive rule can loop. Prolog is this procedure with a fixed search order.

Figure. The query tree, not the firing order. Responsible needs Person and Borrowed; Person needs Student. Sage nodes match facts. Topology of subgoals; not a proof animation.

4Resolution as refutation

Resolution is one inference rule. Written on clauses — disjunctions of literals — it says: from A \vee B and \neg A \vee C, after unifying the complementary pair, derive B \vee C. A fact P is the unit clause P. A query Q is proved by refutation: add \neg Q to the KB and try to derive the empty clause, the clause with no literals, which is unsatisfiable. If you do, the KB plus \neg Q cannot be true, so the KB entails Q.

On the library, to prove Person(Priya) you add \neg \mathrm{Person}(\mathrm{Priya}). The rule \mathrm{Student}(x) \rightarrow \mathrm{Person}(x) is the clause \neg \mathrm{Student}(x) \vee \mathrm{Person}(x). Resolving that with \neg \mathrm{Person}(\mathrm{Priya}) produces \neg \mathrm{Student}(\mathrm{Priya}). Resolving with the fact \mathrm{Student}(\mathrm{Priya}) produces the empty clause. The query is proved. The same rule works on clauses that are not definite — that is the expressiveness the chainers gave up.

Figure. Add ¬Person(Priya) and resolve with ¬Student(x) ∨ Person(x) to get ¬Student(Priya) under {x/Priya}. Resolve that with the fact Student(Priya) to the empty clause. KB ∪ {¬Person(Priya)} is unsatisfiable, so the KB entails Person(Priya).

5Complete, and not a decision procedure

Resolution is sound and, with a fair search and the occur-check, complete for FOL: if the KB entails Q, a refutation will eventually appear. Church and Turing showed the converse fails as a halt: if the KB does not entail Q, the search may run forever. That is the semi-decidability the Knowledge Engineering glimpse already stated, now attached to a procedure you have seen fire.

Production systems and databases stay inside fragments where the search does halt — definite clauses without functions, or description logics with a restricted quantifier. The habit is the same as in search: pick the procedure whose object and whose halt story match the job. Forward when new facts should wake rules. Backward when one query should wake rules. Resolution when the KB is not definite. And do not read a long silence as a proof of \neg Q.

Figure. If the KB entails Q, a fair resolution search with the occur-check will eventually produce a refutation. If it does not, Church and Turing: the search may run forever. Do not read a long silence as a proof of ¬Q.