zlacker

Yeah, it's confusing. The article is referring to the incompleteness of Prolog implemented using Depth First Search. That's what the author means by "backtracking". I know this because I know "backtracking" is used in the logic programming community to stand for DFS, but if you don't know the jargon you'd be right to be confused. You can kind of, er, glean, that meaning in the article if you see how they refer to a "fixed" search strategy, and also notice that "backtracking" is not normally a search strategy since it can't search on its own. "Backtracking" is really "DFS with backtracking".

The article is pointing out that Prolog with backtracking DFS is incomplete with respect to the completeness of SLD-Resolution. To clarify, SLD-Resolution is complete for refutation, or with subsumption. Prolog is an implementation of SLD-Resolution using DFS with backtracking. DFS is incomplete in the sense that it gets stuck in infinite loops when an SLD tree (the structure searched by DFS in Prolog) has cycles, especially left-recursive cycles. The article gives an example of a program that loops forever when executed with DFS with backtracking, in ordinary Prolog.

SLD-Resolution's completeness does not violate the Church-Turing thesis, so it's semi-decidable: SLD-trees may have infinite branches. To be honest I don't know about the equivalence with Horn-SAT, but Resolution, restricted to definite clauses, i.e. SLD-Resolution, is complete (by refutation and subsumption, as I say above, and respecting some structural constraints to do with the sharing of variables in heads and bodies of clauses). We got several different proofs of its completeness so I think we can trust it's true.

Edit: where does this knowledge about Horn-Sat come from? Do you have references? Gimme gimme gimme.