🚀 go-pugleaf

    Prolog does *not* find solutions.  Prolog finds **proofs**, and shows you
    (part of) the substitution it found for each proof.  The goal
	    ?- member(a, [a,a,a]).
    has three proofs.  So that's the number of times Prolog should come back
    to you with an answer substitution.  However, there is a fine point to do
    with the user interface.  Many Prolog systems check the query that you
    type in, and if it hasn't got any variables, just say "yes" or "no".
    NU Prolog does this, except it says "true" or "false".  Transcript:
	    % np
	    NU-Prolog 1.4
	    1?- member(a, [a,a,a]).
	    true.
    However, if you put a variable in there to fool it, you will see that it
    is prepared to find the other proofs.  Transcript:
	    2?- X=dummy, member(a, [a,a,a]).
	    X = dummy ;
	    X = dummy ;
	    X = dummy ;
	    fail.

    Another way of seeing that the three proofs are found is
	    3?- member(a, [a,a,a]), write(*), fail.
	    ***fail.

On the other hand, it seems perfectly reasonable for a PROLOG or any logic
language implementation to note that in the variable case above, reproving
the member doesn't change the binding of X and refuse to do it, rather
simply fail. This is what would happen if "intelligent backtracking" were
being used. Similarly, in the last example, since no variable can be rebound
by the current frame, fail should exit the proof immediately after the first
write.

I think part of the issue is that Prolog really doesn't find "proofs" in the
logical sense, rather it does SLD resolution. That is to say, one shouldn't
confuse PROLOG, which is a programming language, with LOGIC which isn't.
That is, it does not return proof trees. If it did, then techniques like
intelligent backtracking could not be used, nor could "side effects" be
allowed (Side effects in the programming language sense).