Unificación (Lógica)

Natural & Formal Sciences Dictionary
El proceso algorítmico de encontrar una sustitución (mapeo de variables a términos) que haga que dos expresiones simbólicas sean idénticas hasta igualdad sintáctica (o igualdad módulo una teoría); central en razonamiento automático, inferencia de tipos y programación lógica.