Unificación

El proceso de hallar sustituciones para variables que hacen que dos expresiones sintácticas (términos) sean idénticas según el álgebra de términos de una lógica; devuelve una sustitución que asigna variables a términos cuando existe solución.