Prolog: истинный/ложный вывод предиката члена?

Question

Мне интересно, почему предикат Prolog предлагает множество альтернатив (с помощью backtracking ?!), если истина уже была унифицирована для вывода.

Например member(1, [1,2,3]). обеспечивает следующий вывод:

true ; 
false. 

Почему member возвращение ложным после того, как уже выяснилось, что атом 1 действительно является членом списка [1,2,3]?

Еще более запутанной для меня является следующий вывод:

?- member(1, [1,2,3,1]). 
true ; 
true. 

Answer 1

В первом примере, вы просите его, чтобы доказать member(1,[1,2,3]).; поскольку он может, он сообщает true. Когда вы вводите ;, вы просите найти другой способ доказать этот запрос; поскольку он не может, он сообщает false.

Во втором случае первый true является потому, что он нашел один из 1 в списке; второй - потому, что он нашел вторую. Если бы вы снова нажали ;, он вернулся бы с false, так как у него не было других способов доказать запрос. (Примечание. Как указывает @WillNess, вы на самом деле не получаете шанс снова нажать ;, это, вероятно, связано с тем, что реализация member такова, что Prolog знает, что альтернатив нет. Если список не заканчивается 1, вы могли бы снова нажать ;.)