Substituições, Unificação

A aplicação da substituição a uma fórmula W denota-se SUBST(W,s) ou Ws.

Significa que todas as ocorrências das variáveis x1, ..., xn em W são substituídas pelos termos t1, ..., tn.

Duas fórmulas A e B são unificáveis se existe uma substituição s tal que As = Bs. Nesse caso, diz-se que s é uma substituição unificadora.

A substituição unificadora mais geral (ou minimal) é a mais simples (menos extensa) que permite a unificação.