本文有关计算机科学主题。其他学科的条目参见合一 (消歧义)。

在数理逻辑中，特别是应用于计算机科学中，两个项的同一是就特殊化次序而言的并(格的最小上界), 就是说，我们在项的集合上假定一个预序，其中 t* ≤ t 意味着 t* 是通过代换(substitute)在 t 中某些项的一个或多个自由变量而从 t 获得的。s 和 t 的同一 u，如果存在的话，是 s 和 t 二者的代换实例的一个项。s 和 t 的任何公共的代换实例也是 u 的实例。

例如，对于多项式 X 和 Y 可以通过采纳 X = Z 和 Y = Z 而同一到 Z。

In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions.

Depending on which expressions (also called terms) are allowed to occur in an equation set (also called unification problem), and which expressions are considered equal, several framework of unification are distinguished. If higher-order variables, that is, variables representing functions, are allowed in an expression, the process is called higher-order unification, otherwise first-order unification. If a solution is required to make both sides of each equation literally equal, the process is called syntactic or free unification, otherwise semantic or equational unification, or E-unification, or unification modulo theory.