标签：#自动定理证明

合一

在逻辑和计算机科学中，合一（unification），是方程求解表达式之间方程的算法过程。例如，使用 x, y, z 作为变量，单元素集合解的方程{cons(x, cons(x, nil)) = cons(2, y)}是一个语法一阶合一问题，具有替换{x ↦ 2, y ↦ cons(2, nil)}作为其唯一解。 合一算法首先由雅克·埃尔布朗 ( 发现，而第一个正式研究可归因于 ，他使用一阶句法合一作为基本构建块他对一阶逻辑的归结过程的…