将所有出现的 Person1 替换为 bob
Prolog 使用syntactic unification，它从不替换。 free variable 只能绑定一次到一个值。如果看起来一个变量被多次更改，则不是。可以有很多stack frames，并且可以为每个堆栈帧创建一组新的变量。
Trace 有点帮助，但我需要将其翻译成上面示例的形式，并用简单的英语写出和解释步骤。
对于这些事实
plays(alice, leadguitar).
plays(noah, drums).
plays(mike, leadguitar).
plays(mike, drums).
plays(katie, baseguitar).
plays(drew, leadguitar).
plays(drew, baseguitar).
还有这个谓词
combo(Person1,Person2,Person3):-
plays(Person1,X),
plays(Person2,Y),
plays(Person3,Z),
X \= Y,
Y \= Z,
X\=Z.
还有这个查询
combo(mike,alice,drew).
先读SWI-PrologDebugging and Tracing Programs
使用跟踪运行查询，启用统一端口并绑定。
?- visible(+unify).
true.
?- leash(-all).
true.
?- trace.
true.
[trace] ?- combo(mike,alice,drew).
Call: (8) combo(mike, alice, drew)
Unify: (8) combo(mike, alice, drew)
Call: (9) plays(mike, _7040)
Unify: (9) plays(mike, leadguitar)
Exit: (9) plays(mike, leadguitar)
Call: (9) plays(alice, _7040)
Unify: (9) plays(alice, leadguitar)
Exit: (9) plays(alice, leadguitar)
Call: (9) plays(drew, _7040)
Unify: (9) plays(drew, leadguitar)
Exit: (9) plays(drew, leadguitar)
Call: (9) leadguitar\=leadguitar
Fail: (9) leadguitar\=leadguitar
Redo: (9) plays(drew, _7040)
Unify: (9) plays(drew, baseguitar)
Exit: (9) plays(drew, baseguitar)
Call: (9) leadguitar\=leadguitar
Fail: (9) leadguitar\=leadguitar
Redo: (9) plays(mike, _7040)
Unify: (9) plays(mike, drums)
Exit: (9) plays(mike, drums)
Call: (9) plays(alice, _7040)
Unify: (9) plays(alice, leadguitar)
Exit: (9) plays(alice, leadguitar)
Call: (9) plays(drew, _7040)
Unify: (9) plays(drew, leadguitar)
Exit: (9) plays(drew, leadguitar)
Call: (9) drums\=leadguitar
Exit: (9) drums\=leadguitar
Call: (9) leadguitar\=leadguitar
Fail: (9) leadguitar\=leadguitar
Redo: (9) plays(drew, _7040)
Unify: (9) plays(drew, baseguitar)
Exit: (9) plays(drew, baseguitar)
Call: (9) drums\=leadguitar
Exit: (9) drums\=leadguitar
Call: (9) leadguitar\=baseguitar
Exit: (9) leadguitar\=baseguitar
Call: (9) drums\=baseguitar
Exit: (9) drums\=baseguitar
Exit: (8) combo(mike, alice, drew)
true.
Call: (8) combo(mike, alice, drew)
Prolog 查找与查询匹配的谓词。当 Prolog 查找谓词时，它按谓词名称（在本例中为 combo）和 arity（在本例中为 3）搜索，并且只找到一个带有一个子句的谓词。 Prolog 还按照它们在源代码中出现的顺序搜索谓词。它还有更多内容（索引），但解释这个简单的查询不需要这种详细程度。
Unify: (8) combo(mike, alice, drew)
一旦 Prolog 根据谓词名称和数量找到了一个子句/事实，它会检查查询和子句或事实的头部是否可以统一。
mike 与Person1 统一。 Person1 现在绑定到 mike。
alice 与 Person2 统一。 Person2 现在绑定到 alice。
drew 与 Person3 统一。 Person3 现在绑定到 drew。
Call: (9) plays(mike, _7040)
如果前一个语句合一，则调用下一个语句。每个语句本身就是一个查询。因此，将查询 plays(mike,X). 作为独立查询运行与子句中的此语句相同。 plays/2 有很多事实，其中两个匹配 plays(mike,X). Prolog 使用它找到的第一个事实，但是由于有多个事实，因此需要选择一个点。我们将这个特定的选择点称为plays(mike,X) - cp1，并在遇到相应的REDO时返回一个特定的选择点。
Unify: (9) plays(mike, leadguitar)
一旦 Prolog 根据谓词名称和数量找到了一个子句/事实，它会检查查询和子句的头部是否可以统一。
plays 与 plays 合并
mike 与 mike 合并
_7040 与 leadguitar 合并。 _7040 绑定到 leadguitar。
Exit: (9) plays(mike, leadguitar)
这只是完成 Prolog box model 的端口。它显示了Call: (9) plays(mike, _7040) 的结果。该声明没有统一。
Call: (9) plays(alice, _7040)
Unify: (9) plays(alice, leadguitar)
Exit: (9) plays(alice, leadguitar)
alice 的模式相同。爱丽丝只有一个事实，所以没有为她生成的选择点。
Call: (9) plays(drew, _7040)
Unify: (9) plays(drew, leadguitar)
Exit: (9) plays(drew, leadguitar)
drew 的模式相同。由于draw 有两个plays(drew,X). 的事实，因此生成了一个选择点。 plays(drew,X) - cp1
Call: (9) leadguitar\=leadguitar
这是第四条语句X \= Y，X 绑定到leadguitar，Y 绑定到leadguitar
Fail: (9) leadguitar\=leadguitar
由于leadguitar 与leadguitar 没有区别，因此此查询失败。失败时，Prolog 会返回上一个选择点（重做）并尝试寻找另一个解决方案。
Redo: (9) plays(drew, _7040)
记住最后创建的选择点plays(drew,X) - cp1。由于某些事情失败了，因此使用另一种可能的解决方案尝试查询。由于plays(drew,X) 的第一个选择点失败，X 为leadguitar，因此使用第二个事实，plays(drew,baseguitar).
Unify: (9) plays(drew, baseguitar)
只是表明plays(drew,X) 的第二个事实正在被使用。
Exit: (9) plays(drew, baseguitar)
它显示了Redo: (9) plays(drew, _7040) 的结果。
剩下的只是对已经完成的内容进行更多的复制/粘贴，并更改语句、变量、绑定值等。
这个answer 类似，但有更多细节。
值得注意的是这个问题
我编写了一个名为 combo 的新规则，用于确定三个人是否可以与鼓手、基础吉他和主音吉他进行组合。
此查询未回答
combo(Person1,Person2,Person3):-
plays(Person1,X),
plays(Person2,Y),
plays(Person3,Z),
X \= Y,
Y \= Z,
X\=Z.
因为如果加上这些事实
plays(alice, flute).
plays(noah, cello).
plays(mike, trumpet).
这个查询
?- combo(alice,noah,mike).
true ;
true .
说的是真的，但 alice、noah 和 mike 没有演奏主吉他、鼓和贝斯吉他。