合一

考虑由变量和常数使用函数符号构建的表达式。如果 , ..., 是变量，且 , ..., 是表达式，那么变量和表达式之间的一组映射 被称为替换。

如果 且 是一个表达式，那么 被称为 的一个实例，如果它是通过同时将 中所有出现的 (对于 ) 替换为相应的 而得到的。

如果 且 是两个替换，那么 和 的组合 (记为 ) 是通过从 中移除所有满足 且 的元素 以及所有满足 是 , ..., 其中之一的元素 而得到的。

如果对于表达式集合 ，替换 满足 ，则称 为该集合的合一器。如果对于同一表达式集合的任何其他合一器 ，都存在另一个合一器 使得 ，则称表达式集合 的合一器 为最一般合一器。

合一算法将表达式集合作为输入。如果此集合不可合一，算法终止并产生否定结果。如果输入表达式集合存在合一器，算法将产生此集合的最一般合一器。合一算法是归结原理的工具。它也是项重写系统的基础。