我有以下条款：
T1 = f(f(3,Z,2),f(I,Z,G),Z)
T2 = f(F,f(R,f(5,2),D),f(3,2,F))
我必须统一这些术语。
我的想法是：
G=(3,Z,2)
I=(5,2)
I=(3,2,F)
我知道如何在简单的例子中统一。任何人都可以为我阐明这一点吗？谢谢
【问题讨论】：
标签： prolog unification
在 Prolog 世界内外培养统一直觉非常有价值。所以我认为花时间学习如何手动找到统一的术语是非常有价值的！统一的奇妙之处在于，您可以使用几何直觉通过统一简单的术语进行推理！
考虑一下来自wikipedia article on unification 的这个可爱的插图以获得一些灵感：
给定两个部分结构，t1 和 t2，我们可以通过比较结构的各个部分来匹配一个中的缺失位和另一个中的现有位来找到统一符。在 Prolog 中，结构中缺少的位是 变量。
回到你的问题，让我们做一些 ascii 艺术，让你的两个术语的结构更加明显。
T1 = f( f(3, R, 2), f(A, R ,I), A )
% | | | | | | |
T2 = f( N , f(E, f(5, 2),S), f(3, 2, N) )
这显示了完全相同的复合术语，只是它们被隔开，并且我添加了匹配术语部分的管道，这些部分必须协调以找出统一性。请注意，管道还连接非变量的术语。这很重要，因为如果结构中有任何不匹配的基本项，那么我们的统一就会失败。
从左到右阅读，我们遇到的第一个变量是N。顺着管道，我们看到N必须与复合词f(3, R, 3)统一，否则结构不可能匹配，统一就会失败。所以我们知道N = f(3, R, 3)。
接下来出现的变量是A 和E。确实，这些是协调的，所以我们知道A = E，但我们还没有足够的信息可以说更多。
我们看到的下一个变量是R。这与复合术语f(5, 2) 协调，所以我们必须有R = f(5, 2)。这给了我们第一次将变量与基本项统一起来！由于我们知道必须与R 统一的基本术语，我们还可以填补我们之前统一N 中的缺失漏洞：N = f(3, R, 4) = f(3, f(5, 2) 3)。
以这种方式继续，您最终会得到 Prolog 为您找到的相同结果，如 Daniel Lyons 的回答所示！
愿你在未来的统一中玩得开心:)
【讨论】：
我很惊讶你不只是让 Prolog 为你做这件事：
?- T1 = f(f(3,R,2),f(A,R,I),A), T2 = f(N,f(E,f(5,2),S),f(3,2,N)), T1=T2.
T1 = T2, T2 = f(f(3, f(5, 2), 2), f(f(3, 2, f(3, f(5, 2), 2)), f(5, 2), S), f(3, 2, f(3, f(5, 2), 2))),
R = f(5, 2),
A = E, E = f(3, 2, f(3, f(5, 2), 2)),
I = S,
N = f(3, f(5, 2), 2).
【讨论】：