Unificação, em ciência da computação e na lógica, é um processo algorítmico de solução de equações entre expressões simbólicas.

Dependendo de quais expressões (também chamadas de termos) são permitidas ocorrer em um conjunto de equações (também chamado de problema da unificação), e quais expressões são consideradas iguais, diversas estruturas de unificação são distinguidas. Se variáveis de alta ordem, isto é, variáveis que representam funções, são permitidas em uma expressão, o processo é chamado de unificação de alta ordem, ou, caso contrário, é chamado de unificação de primeira ordem. Se exige-se uma solução que faça com que ambos os lados de cada equação sejam literalmente iguais, o processo é chamado de unificação sintática, ou, caso contrário, unificação semântica, ou unificação equacional, ou unificação E, ou unificação módulo uma teoria.

A solução de um problema de unificação é denotada como uma substituição, isto é, um mapeamento atribuindo um valor simbólico a cada variável das expressões do problema. Um algoritmo de unificação deve computar, para um dado problema, um conjunto de substituição completo e mínimo, isto é, um conjunto cobrindo todas as soluções e com nenhum membro redundante. Dependendo da estrutura, um conjunto de substituição completo e mínimo talvez contenha nenhum, ou uma quantidade finita, ou infinita de membros. ^[nota1] Em algumas estruturas é geralmente impossível decidir se existe alguma solução. Para a unificação sintática de primeira ordem, Martelli e Montanari desenvolveram um algoritmo capaz de informar a inexistência de uma solução ou computar um único conjunto de substituição completo e mínimo contendo o chamado unificador mais geral.

Por exemplo, usando x, y, z como variáveis e o único conjunto de equação { cons(x,cons(x,nil)) = cons(2,y) } é um problema unificação sintática de primeira ordem que tem a substituição { x ↦ 2, y ↦ cons(2,nil) } como uma única solução. O problema da unificação sintática de primeira ordem { y = cons(2,y) } não possui uma solução sobre o conjunto de termos finitos; contudo, possui como solução única { y ↦ cons(2,cons(2,cons(2,...))) } sobre o conjunto de árvores infinitas. O problema da unificação semântica de primeira ordem { a⋅x = x⋅a } possui toda substituição da forma { x ↦ a⋅...⋅a } como uma solução em um semi grupo, isto é, se (⋅) é considerado associativo; o mesmo problema, visto em um grupo abeliano, onde (⋅) é considerado também como comutativo, tem qualquer substituição como uma solução. O único conjunto { a = y(x) } é um problema se unificação sintático de segunda ordem, desde que y seja uma função variável. Uma solução é { x ↦ a, y ↦ (função identidade) }; outra solução é { y ↦ (função constante mapeando cada valor para a), x ↦ (qualquer valor) }.

A primeira investigação formal de unificação pode ser atribuída a John Alan Robinson, quem usou a unificação sintática de primeira ordem como um bloco básico de construção em seu processo de resolução para a lógica de primeira ordem, um bom avanço na tecnologia de raciocínio automatizado, uma vez que isso eliminou uma fonte de explosão combinatória: busca por instanciação de termos. Hoje, o raciocínio automatizado continua sendo a principal área de aplicação da unificação. A unificação sintática de primeira ordem é usada na lógica de programação e na implementação de sistema de tipos na linguagem de programação, especialmente nos tipos de algoritmos de inferência baseados em Hindley–Milner. A unificação semântica é usada em solucionadores SMT e em algoritmos de reescrita de termos. Unificação de alta ordem é usada em assistentes de provas, por exemplo, Isabelle e Twelf, e formas restritas da unificação de alta ordem (padrão de unificação de alta ordem) são usadas em algumas implementações de linguagens de programação, no caso de lambdaProlog. Como padrões de alta ordem são expressivos, seu processo de unificação associada ainda retêm propriedades teóricas próximas a unificação de primeira ordem.