As a general matter, you can't prove a predicate true or false by automatic means. Logic programming is just as "artful" as imperative or functional programming, because they all run into the same problem: it's impossible to tell the difference between long-running and infinite computation. The question of algorithms for general logic was explicitly addressed as the Entscheidungsproblem, meaning decision problem, which was independently proven undecidable by both Turing and Church:
>> As a general matter, you can't prove a predicate true or false by automatic means.
Not in the general case, sure, yet in practice I'm sure we've all written plenty of code that terminates just fine. [Edit: I'm talking about imperative as well as logic or functional programming code].
The question then is- what does it mean when a program terminates? In the case of principled approaches like logic or functional programming, you have a pretty good idea what that means (e.g. a logic program proves a theory true or false). When an imperative program terminates, it's a very hairy affair to say what, exactly, termination means.
[Edit 2: Actually, if you think about it, there's nothing we can really achieve in the general case (including machine learning; see language learning in the limit). In practice, on the other hand, we're doing things, alright - by continuously relaxing principles and fudging limits as necessary (see PAC learning)].
https://en.wikipedia.org/wiki/Entscheidungsproblem