I am wondering why the member/2 predicate of Prolog delivers multiple alternatives (via backtracking?!), if true was already unified for the output.
For example member(1, [1,2,3]). delivers the following output:
true ;
false.
Why does member return false after it already found out that the atom 1 is indeed a member of the list [1,2,3]?
Even more confusing to me is the following output:
?- member(1, [1,2,3,1]).
true ;
true.
In your first example, you ask it to prove member(1,[1,2,3]).; since it can, it reports true. When you enter ;, you are asking to find another way to prove that query; since it cannot, it reports false.
In the second case, the first true is because it found one of the 1's in the list; the second is because it found the second. If you had hit ; again, it would have come back with false, as it had no other ways to prove the query. (Note: As @WillNess points out, you don't actually get the chance to hit ; again; this is probably due to the implementation of member being such that Prolog knows there are no remaining alternatives. If the list did not end with a 1, you would be able to hit ; again.)
memberd/2. – false