A couple terminological nits: Logic programs are sets of clauses so in Prolog, all your code is a set of clauses, not "a glorified horn clause", as you say. Ho

A couple terminological nits: Logic programs are sets of clauses so in Prolog, all your code is a set of clauses, not "a glorified horn clause", as you say. Horn clauses are the components of a logic program. Horn clauses can be interpreted as implications, "A IF B AND C AND D..." or "A IF (empty)" or "(empty) IF A". The first two are known as definite clauses and the last as a goal, or, in more database-y terminology, as "rules", "facts" and "queries". A logic program is written as a set of "facts" and "rules" and executed by running a "query" over it. Now all this is to say that Horn clauses aren't "limited". There are First-Order Logic (FOL) expressions that can't be encoded in Horn logic (e.g. "A OR B" where neither A nor B are negated), but definite clauses are sound and refutation-complete for SLD-resolution, a deductive procedure. Soundess means that any statement found true, is true; and completeness means that any true statement can be found true. In plain English, the restriction to Horn clauses is only syntactic and you can express anything, in a logic programming language, that can be expressed in any language in which you can encode a Universal Turing Machine. With apologies for the nitpicking :) Edit: As to the use of depth-first search (DFS), it's not that the space of Horn clauses is searched. That is what is done in Inductive Logic Programming where the goal is to find new programs. In the garden variety Logic Programming, which is deductive, DFS is used to find _resolvents_, which are literals (elements of clauses) with opposite signs (positive or negative) that are elminated to eventually reduce a query down to the empty-clause. If this can be done, then the query is refuted. Since a query is basically a set of negated literals, a successful refutation proves it (well, actually, it proves its _complement_; but this is what we usually want to prove). Searching for resolents is actually pretty efficient because the set of possible resolvents keeps getting smaller as one goes. Unless one gets stuck in an infinite loop, of course, which is a limitation of DFS. But, as the paper hints, there are other execution strategies, such as SLG-resolution, which can avoid some of that. Edit 2: Regarding higher-order logics, Prolog is normally described as a FOL language but in truth it cheats and allows higher-order variables. In particular, it allows variables quantified over _logic programs_. Which is definitely very much above the first-order. But that's a super big secret that should never be revealed to anyone outside logic programming circles. Ever.