I don't disagree with what you say here, but ... I'm coming at it from a formal semantics point of view. (I find Prolog and indeed "logic programming" in a larger sense to be all promise and little delivery on this front.) Perhaps you can check if your `prove` example is expressible in HiLog ... if so, it's more-or-less first order (in a semantically clean way). I believe the hard working XSB have an implementation.
I don't know that Prolog, or logic programming, makes any promises about formal semantics. I have to say I don't think of Prolog or logic programming in that context. Except for the more general point that Prolog programs are theories, and when a query is executied, that's a theorem being proven.
Btw, I'm not at all complaining about Prolog's higher-order. That may be a "hidden" feature, but it's a really, really useful one. FOL is actually very restrictive in many ways. As far as I understand it, the distinction between first and higher-order logics was not made by Peirce and Frege, who tended to fudge the orders a lot, just like Prolog.
In any case, for me, logic programming begins and ends with Robinson's paper on Resolution. That was not about formal semantics, and only about a sound and complete inference rule. And that (soundness and completeness) is all I really need to know. The rest (including definite clauses, SLD-Resolution and Prolog) is all implementation details.
