Lógicas Clássicas

Resolução
- Duas fórmulas-atômicas são contraditórias se uma delas puder ser unificada com o não da outra. Assim, por exemplo, Homem(x) e ? Homem(Spot) podem ser unificados.
- Isto corresponde à intuição que diz que não pode ser verdadeiro para todos os x, que Homem(x) se houver conhecimento de haver algum x, digamos Spot, para o qual Homem(x) é falso.
- Na lógica de predicados utilizaremos o algoritmo de unificação para localizar pares de fórmulas-atômicas que se cancelem.

Resolução