合一是数理逻辑中的一阶谓词演算使用的一种运算方法。数理逻辑就是以推理(特别是数学中的演绎推理)作为研究对象的学科,它主要是运用数学方法使用数学符号,来研究数学领域公共使用的逻辑推理。而在语言研究中使用“合一”法,就是要用数理逻辑的推理方式来描述语言,达到精确化的目的。
简介
在数理逻辑中，特别是应用于计算机科学中，两个项的同一是就特殊化次序而言的并(格的最小上界),就是说，我们在项的集合上假定一个预序，其中意味着是通过代换(substitute)在中某些项的一个或多个自由变量而从获得的。和的同一，如果存在的话，是和二者的代换实例的一个项。和的任何公共的代换实例也是的实例。
例如，对于多项式和可以通过采纳和而同一到。
Prolog 中的合一
同一
由于它的声明本性，一序列合一的次序(通常)是不重要的。
注意在一阶逻辑的术语中，原子是基本命题而且其合一同Prolog项一样。
合一的例子
:成功(重言式)
:和二者合一于原子
:合一是对称的
:合一成功
:合一失败，因为原子是不同的
:合一于
:失败，因为项的头部是不同的
:合一失败，因为项有不同的元数
:合一于项
:合一于原子而合一于项
:无限合一，合一于。在严格的一阶逻辑和很多现代Prolog方言中，这是禁止的(并由出现检查来强制)
:合一失败；效果上