Forward Chaining Is Complete for Horn Clauses
Claim
Let \(KB\) be a knowledge base of definite Horn clauses (facts and rules). Forward chaining derives every ground atom entailed by \(KB\). That is, if \(KB \models q\) then forward chaining adds \(q\) to \(\mathit{known}\) before terminating (Russell and Norvig 2020).
Proof
Let \(FC\) denote the set of ground atoms in \(\mathit{known}\) at the fixed point of forward chaining (when the agenda is empty and no new atoms can be added).
Step 1: \(FC\) is a model of \(KB\).
We check that every clause in \(KB\) is satisfied under \(FC\):
- Facts: every base fact is added to \(\mathit{known}\) at initialization, so all facts are in \(FC\).
- Rules: consider any rule \(p_1 \land \cdots \land p_n \Rightarrow q\). Suppose all premises \(p_i \in FC\). Then when the last \(p_i\) was added to \(\mathit{known}\), the algorithm checked this rule and found all premises satisfied; since \(q \notin FC\) would have caused \(q\) to be added, we must have \(q \in FC\). So the rule is satisfied.
Therefore \(FC \models KB\).
Step 2: \(FC\) is the minimal model of \(KB\).
Let \(M\) be any model of \(KB\). We show \(FC \subseteq M\) by induction on the order in which atoms are added to \(FC\):
- Every base fact is in \(M\) (since \(M \models KB\) and facts are clauses).
- If \(p_1, \ldots, p_n \in M\) and the rule \(p_1 \land \cdots \land p_n \Rightarrow q\) is in \(KB\), then \(q \in M\) (since \(M\) satisfies the rule). So each atom added to \(FC\) by rule firing is also in \(M\).
Therefore \(FC \subseteq M\) for every model \(M\) of \(KB\).
Step 3: Completeness.
If \(KB \models q\), then \(q\) is true in every model of \(KB\). In particular, \(q \in M\) for every model \(M\). By Step 2, \(FC \subseteq M\) for all \(M\); but we need the reverse: \(q \in FC\).
Suppose for contradiction that \(q \notin FC\). Then \(FC\) is a model of \(KB\) (by Step 1) in which \(q\) is false. This contradicts \(KB \models q\). Therefore \(q \in FC\), and forward chaining derives \(q\). \(\blacksquare\)
Note on First-Order Horn Clauses
The same argument applies to first-order definite Horn clauses without function symbols (Datalog): the Herbrand base is finite, forward chaining reaches a fixed point, and the fixed point is the minimal Herbrand model. With function symbols the Herbrand base may be infinite and forward chaining need not terminate, but the fixed point remains the minimal model whenever it exists.