云昴
[Learn Prolog Now 2] Unification and Proof Search
本文英文原文： http://www.learnprolognow.org/ 并会增加自己在Imperial学习中的一些想法，因为自己已经熟悉Prolog，并非完整翻译。
合一
如果term1和term2都是常量，那么term1和term2能够合一，当且仅当它们是相同的原子，或者相同的数字。
如果term1是变量并且term2是任意类型的语句，那么term1和term2能够合一，并且term1被初始化为term2；同理，如果term2是变量并且term1是任意类型的语句，那么term1和term2能够合一，并且term2被初始化为term1。（如果两个都是变量，他们都能够被互相初始化，即它们共享相同的值）
如果term1和term2都是复杂语句，那么它们能够合一当且仅当：
3.1 它们有相同的函子和元数；
3.2 所有对应的参数能够合一；
3.3 变量的初始化能够匹配。（比如，如果两个复杂语句在进行合一，不可能在一个复杂语句中将X初始化为mia，在另外一个复杂语句中将X初始化为vincent）
两个语句能够合一当且仅当它们遵循上面三个定义之一。
特殊的例子1
?- X = Y.
Prolog会如何回答？这依赖不同的Prolog实现，在我的机器上，SWI-Prolog会回答：
X = Y
即简单地认为X和Y可以合一，因为变量可以和任意类型的语句合并，如果变量和变量合一，表示它们分享同样的值。另外，可能其他Prolog实现会这么回答：
X = _5071
Y = _5071
true
这里发生了什么？本质上，和之前的第一个回答是一致的。注意_5071是一个变量（以下划线开头），合一的定义子句2告诉我们，如果两个变量合一，它们会共享一个值，所以Prolog就创建了一个新的值（名字是_5071），X和Y都共享这个值。不必在意_5071的实际值，它仅仅是表示X和Y有相同的值，这个值可能是另外的变量，比如_5075，或者_6189。
特殊的例子2
?- X = mia, X = vincent.
Prolog会回答false。这个查询包含了两个目标，X = mia和 X = vincent，分开来看，Prolog会认为两个目标都成功，首先将X初始化为mia，然后是vincent。但是这里存在问题：一旦Prolog尝试满足第一个目标，X被初始化为mia，它就不能再和vincent合一了（变量只能初始化一次）。所以第二个目标会失败，一个已经初始化的变量不再是变量了，它已经变成了它初始化的值。