Substituição simultânea (de variáveis por termos). Pares de termos unificáveis. Sete exemplos. Substituição unificadora mais geral (mgu: most general unifier). Algoritmo de unificação mais geral: um exemplo.