在邏輯學和計算機科學中，統一是解決符號表達式之間方程的一個算法過程。根據哪些表達式（也叫術語）允許出現在方程組中（也叫統一問題），以及哪些表達式被認為是相等的，可以區分出幾個統一的框架。如果一個表達式中允許出現高階變量，即代表函數的變量，那么這個過程被稱為高階統一，否則稱為一階統一。如果一個解決方案需要使每個等式的兩邊都相等，那么這個過程就被稱為句法或自由統一，否則就被稱為語義或等式統一，或E-統一，或統一模態理論。統一問題的解決方案被稱為替換，即為問題表達式中的每個變量分配一個符號值的映射。統一算法應該為一個給定的問題計算出一個完整的、最小的替換集，即一個包含問題的所有解決方案的集合，并且沒有多余的成員。根據不同的框架，一個完整的最小替換集可能最多只有一個，最多只有有限的幾個，或者可能有無限多的成員，或者根本就不存在。在某些框架中，通常無法決定是否存在任何解決方案。對于一階句法統一，Martelli和Montanari給出了一種算法，它可以報告不可解性，或者計算出一個完整的、最小的單子替換集，其中包含所謂的最一般的統一器。例如，用x,y,z作為變量，單子方程組{cons(x,cons(x,nil))=cons(2,y)}是一個句法一階統一問題，它的xxx解是替換{x?2,y?cons(2,nil)}。句法一階統一問題{y=cons(2,y)}在有限項集合上沒有解；然而，它在無限樹集合上有xxx的解{y?cons(2,cons(2,cons(2,...))語義一階統一問題{a?x=x?a}在半群中，即如果(?)被認為是關聯的，則每個替換形式{x?a?...?a}都是一個解決方案；同樣的問題，在非線性群中，即(?)被認為是換元的，有任何替換都是一個解決方案。單子集{a=y(x)}是一個語法上的二階統一問題，因為y是一個函數變量。一個解決方案是{x?a,y?(身份函數)}；另一個解決方案是{y?(常數函數將每個值映射到a),x?(任何值)}。統一算法最早是由JacquesHerbrand發現的，而xxx次正式研究可以歸功于JohnAlanRobinson，他將一階句法統一作為他的一階邏輯的解析程序的基本構件，這是自動推理技術的一大進步，因為它消除了組合爆炸的一個來源：搜索術語的實例化。今天，自動推理仍然是統一的主要應用領域。

語法上的一階統一被用于邏輯編程和編程語言類型系統的實現，特別是基于Hindley-Milner的類型推理算法。語義上的統一被用于SMT求解器、術語重寫算法和加密協議分析。高階統一用于證明助手，例如Isabelle和Twelf，高階統一的限制形式（高階模式統一）用于一些編程語言的實現，例如lambdaProlog，因為高階模式具有表達能力，但其相關的統一程序保留了更接近一階統一的理論屬性。

從形式上看，統一方法的前提是一個無限的集合V{displaystyleV}的變量。的變量。對于高階統一，方便的做法是選擇{displaystyleequiv}反映了關于某些函數符號的背景知識；例如，如果是一個人，那么他就會被認為是一個人。