合一

考慮由變數和常數使用函式符號構建的表示式。如果 , ..., 是變數，且 , ..., 是表示式，那麼變數和表示式之間的一組對映 被稱為替換。

如果 且 是一個表示式，那麼 被稱為 的一個例項，如果它是透過同時將 中所有出現的 (對於 ) 替換為相應的 而得到的。

如果 且 是兩個替換，那麼 和 的組合 (記為 ) 是透過從 中移除所有滿足 且 的元素 以及所有滿足 是 , ..., 其中之一的元素 而得到的。

如果對於表示式集合 ，替換 滿足 ，則稱 為該集合的合一器。如果對於同一表示式集合的任何其他合一器 ，都存在另一個合一器 使得 ，則稱表示式集合 的合一器 為最一般合一器。

合一演算法將表示式集合作為輸入。如果此集合不可合一，演算法終止併產生否定結果。如果輸入表示式集合存在合一器，演算法將產生此集合的最一般合一器。合一演算法是歸結原理的工具。它也是項重寫系統的基礎。