I used interpretation as it occurs for example in Computability and Logic by Boolos, Burgess and Jeffrey. It is also explained here: https://en.wikipedia.org/w

I used interpretation as it occurs for example in Computability and Logic by Boolos, Burgess and Jeffrey. It is also explained here: https://en.wikipedia.org/wiki/Interpretation_(logic)#Interpretations_of_a_first-order_language https://en.wikipedia.org/wiki/Interpretation_(logic)#Interpr... Please note that from a logical perspective, a (pure) Prolog program is always a set of first-order clauses, since all variables that occur in a Prolog program are implicitly quantified to range over individuals and hence terms, not over predicates or sets of predicates etc., which would be characteristic of second- and higher-order logic. This also includes meta-calls and meta-predicates! This is because, in Prolog, if a variable P occurs as a goal anywhere, it is interpreted as call(P), i.e., a universally quantified variable that is the argument of the predicate call/1. And call/1 is expressible in first-order logic, using at most one clause per predicate: call(true). call(X = Y) :- X = Y. call(dif(X,Y)) :- dif(X, Y). call(X #= Y) :- X #= Y. etc. So, even though Prolog programmers call predicates involving meta-calls "higher-order" programming (since predications are passed as arguments), it is not an instance of higher-order reasoning from a logical perspective. An example of a logical higher-order statement must quantify (at least) over predicates, so for example "For all unary predicates, the induction axiom is true." There is no way to express this in Prolog, because its universally quantified variables implicitly always range exclusively over domain elements (Herbrand terms), and you cannot quantify over predicates. Regarding all-solutions predicates like setof/3, which are also higher-order predicates in the sense of Prolog: These predicates are not monotonic (for example, adding a fact may cause a query to fail that previously succeeded), and they therefore do not correspond to predicates in classical logic, where entailment is monotonic.