Lógicas Clássicas
Resolução
RESOLUÇÃO NA LÓGICA DOS PREDICADOS
- Na Lógica Proposicional é fácil determinar que dois literais não possam ser verdadeiros ao mesmo tempo. (Simplesmente procure L e ? L)
- Na Lógica dos Predicados este processo de casamento (“matching”) é mais complicado.Por exemplo Homem(Henry) e ? Homem(Henry) é uma contradição, enquanto que Homem(Henry) e ?Homem(Spot) não o é.
- Assim, para determinar contradições, precisamos de um procedimento de matching que compare dois literais e descubra se existe um conjunto de substituições que os torne idênticos.
- O ALGORITMO DE UNIFICAÇÃO é um procedimento recursivo direto que faz exatamente isto.