>> You hard code some options, write a logical condition with placeholders, and Prolog brute-forces every option in every placeholder. It doesn't do reasoning.
SLD-Resolution with unification (Prolog's automated theorem proving algorithm) is the polar opposite of brute force: as the proof proceeds, the cardinality of the set of possible answers [1] decreases monotonically. Unification itself is nothing but a dirty hack to avoid having to ground the Herbrand base of a predicate before completing a proof; which is basically going from an NP-complete problem to a linear-time one (on average).
Besides which I find it very difficult to see how a language with an automated theorem prover for an interpreter "doesn't do reasoning". If automated theorem proving is not reasoning, what is?
> "as the proof proceeds, the cardinality of the set of possible answers [1] decreases"
In the sense that it cuts off part of the search tree where answers cannot be found?
member(X, [1,2,3,4]),
X > 5,
slow_computation(X, 0.001).
will never do the slow_computation - but if it did, it would come up with the same result. How is that the polar opposite of brute force, rather than an optimization of brute-force?
If a language has tail call optimization then it can handle deeper recursive calls with less memory. Without TCO it would do the same thing and get the same result but using more memory, assuming it had enough memory. TCO and non-TCO aren't polar opposites, they are almost the same.
Rather, in the sense that during a Resolution-refutation proof, every time a new Resolution step is taken, the number of possible subsequent Resolution steps either gets smaller or stays the same (i.e. "decreases monotonically"). That's how we know for sure that if the proof is decidable there comes a point at which no more Resolution steps are left, and either the empty clause is all that remains, or some non-empty clause remains that cannot be reduced further by Resolution.
So basically Resolution gets rid of more and more irrelevant ...stuff as it goes. That's what I mean that it's "the polar opposite of brute force". Because it's actually pretty smart and it avoids doing the dumb thing of having to process all the things all the time before it can reach a conclusion.
Note that this is the case for Resolution, in the general sense, not just SLD-Resolution, so it does not depend on any particular search strategy.
I believe SLD-Resolution specifically (which is the kind of Resolution used in Prolog) goes much faster, first because it's "[L]inear" (i.e. in any Resolution step one clause must be one of the resolvents of the last step) and second because it's restricted to [D]efinite clauses and, as a result, there is only one resolvent at each new step and it's a single Horn goal so the search (of the SLD-Tree) branches in constant time.
Refs:
J. Alan Robinson, "A computer-oriented logic based on the Resolution principle" [1965 paper that introduced Resolution]
I don't want to keep editing the above comment, so I'm starting a new one.
I really recommend that anyone with an interest in CS and AI read at least J. Alan Robinson's paper above. For me it really blew my mind when I finally found the courage to do it (it's old and a bit hard to read). I think there's a trope in wushu where someone finds an ancient scroll that teaches them a long-lost kung-fu and they become enlightened? That's how I felt when I read that paper, like I gained a few levels in one go.
Resolution is a unique gem of symbolic AI, one of its major achievements and a workhorse: used not only in Prolog but also in one of the two dominant branches of SAT-Solving (i.e. the one that leads from Hillary-Putnam to Conflict Driven Clause Learning) and even in machine learning, in of the two main branches of Inductive Logic Programming (which I study) and which is based on trying to perform induction by inverting deduction and so by inverting Resolution. There's really an ocean of knowledge that flows never-ending from Resolution. It's the bee's knees and the aardvark's nightgown.
I sincerely believe that the reason so many CS students seem to be positively traumatised by their contact with Prolog is that the vast majority of courses treat Prolog as any other programming language and jump straight to the peculiarities of the syntax and how to code with it, and completely fail to explain Resolution theorem proving. But that's the whole point of the language! What they get instead is some lyrical waxing about the "declarative paradigm", which makes no sense unless you understand why it's even possible to let the computer handle the control flow of your program while you only have to sort out the logic. Which is to say: because FOL is a computational paradigm, not just an academic exercise. No wonder so many students come off those courses thinking Prolog is just some stupid academic faffing about, and that it's doing things differently just to be different (not a strawman- actual criticism that I've heard).
In this day and age where confusion reigns about what even it means to "reason", it's a shame that the answer, that is to be found right there, under our noses, is neglected or ignored because of a failure to teach it right.
The way to learn a language is not via its syntax but by understanding the computation model and the abstract machine it is based on. For imperative languages this is rather simple and so we can jump right in and muddle our way to some sort of understanding. With Functional languages it is much harder (you need to know logic of functions) and is quite impossible with Logic languages (you need to know predicate logic) Thus we need to first focus on the underlying mathematical concepts for these categories of languages.
The Robert Kowalski paper Predicate Logic as a Programming Language you list above is the Rosetta stone of logic languages and an absolute must-read for everybody. It builds everything up from the foundations using implication (in disjunctive form), clause, clausal sentence, semantics, Horn clauses and computation (i.e. resolution derivation); all absolutely essential to understanding! This is the "enlightenment scroll" of Prolog.
I don't understand (the point of) your example. In all branches of the search `X > 5` will never be `true` so yeah `slow_computation` will not be reached. How does that relate to your point of it being "brute force"
>> but if it did, it would come up with the same result
Meaning either changing the condition or the order of the clauses. How do you expect Prolog to proceed to `slow_computation` when you have declared a statement (X > 5) that is always false before it.
The point is to compare a) evaluate all three lines (member, >5, slow_computation) then fail because the >5 test failed; against b) evaluate (member, >5) then fail. And to ask whether that's the mechanism YeGoblynQueyne is referring to. If so, is it valid to describe b as "the polar opposite" of a? They don't feel like opposites, merely an implementation detail performance hack. We can imagine some completely different strategy such as "I know from some other Constraint Logic propagation that slow_computation has no solutions so I don't even need to go as far as the X>5 test" which is "clever" not "brute".
> "How do you expect Prolog to proceed to `slow_computation` when you have declared a statement (X > 5) that is always false before it"
I know it doesn't, but there's no reason why it can't. In a C-like language it's common to do short-circuit Boolean logic evaluation like:
A && B && C
and if the first AND fails, the second is not tested. But if the language/implementation doesn't have that short-circuit optimisation, both tests are run, the outcome doesn't change. The short-circuit eval isn't the opposite of the full eval. And yes this is nitpicking the term "polar opposite of" but that's the relevant bit about whether something is clever or brute - if you go into every door, that's brute. If you try every door and some are locked, that's still brute. If you see some doors have snow up to them and you skip the ones with no footprints, that's completely different.
SLD-Resolution with unification (Prolog's automated theorem proving algorithm) is the polar opposite of brute force: as the proof proceeds, the cardinality of the set of possible answers [1] decreases monotonically. Unification itself is nothing but a dirty hack to avoid having to ground the Herbrand base of a predicate before completing a proof; which is basically going from an NP-complete problem to a linear-time one (on average).
Besides which I find it very difficult to see how a language with an automated theorem prover for an interpreter "doesn't do reasoning". If automated theorem proving is not reasoning, what is?
___________________
[1] More precisely, the resolution closure.