合一是数理逻辑中的一阶谓词演算使用的一种运算方法。数理逻辑就是以推理(特别是数学中的
演绎推理)作为研究对象的学科,它主要是运用数学方法使用数学符号,来研究数学领域公共使用的逻辑推理。而在语言研究中使用“合一”法,就是要用数理逻辑的推理方式来描述语言,达到精确化的目的。
在数理逻辑中,特别是应用于
计算机科学中,两个项的同一是就特殊化次序而言的并(格的最小上界),就是说,我们在项的集合上假定一个预序,其中意味着是通过代换(substitute)在中某些项的一个或多个自由变量而从获得的。和的同一,如果存在的话,是和二者的代换实例的一个项。和的任何公共的代换实例也是的实例。
同一概念是在
Prolog背后的主要想法。它表示绑定变量的内容的机制并可以看作为一种只一次的(one-time)赋值。在Prolog中,这种操作用符号"="来指示。
1.在传统Prolog中,未实例化的变量—就是说在它上面以前没有进行合一,可以合一于一个原子、一个项、或另一个未实例化的变量,因此在效果上变成了它的别名。在很多现代Prolog方言和
一阶逻辑演算中,变量不能合一于包含它的项;这叫做出现检查。