= Solution
The algorithm is $\boxed{\text{incorrect: it can return true for a non-entailed ground atom}}$. Its recursive calls return only Booleans. They do not return and propagate the <first-order substitutions> obtained while satisfying earlier rule premises.
Take distinct constants $a,b,c$, facts
$$
\mathcal F=\{P(a),Q(b)\},
$$
and the single <Datalog> rule
$$
P(x)\land Q(x)\to H(c).
$$
Ask for $H(c)$. The head matches the goal without binding $x$. In line 15, the recursive call for $P(x)$ succeeds by <first-order unification> with $P(a)$, but returns only `true`. The next recursive call still receives $Q(x)$ with $x$ unbound, and succeeds by <first-order unification> with $Q(b)$. Neither subgoal is the visited head $H(c)$, so the visited test does not stop these calls. Both recursive results are `true`, and the algorithm returns `true` for $H(c)$.
However, the <least Herbrand model> is just $\{P(a),Q(b)\}$. No single constant makes both $P(x)$ and $Q(x)$ true, so the rule cannot derive $H(c)$. The two individually successful premises need one consistent <first-order substitution>. A correct <backward chaining> procedure must thread answer <first-order substitutions> through the remaining premises and backtrack when they cannot be extended; <forward chaining> on ground <Datalog> instances is another way to avoid this error.
Back to article page
