–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.
–O ALGORITMO DE UNIFICAÇÃO
–Para apresentar a unificação, consideramos as fómulas como lista em que o primeiro elemento é o nome do predicado e os elementos restantes são os argumentos.
–Exemplo:
•(TentarAssassinar Marco Cesar)
•(TentarAssassinar Marco (Soberanode Roma))
–Para tentar unificar dois literais, primeiro conferimos se seus primeiros elementos são iguais. Caso contrário não há meio de serem unificados.
–Se o primeiro casar, podemos continuar com o segundo e assim por diante.
–Constantes, funções e predicados diferentes não podem casar, os idênticos podem. Uma variável pode casar com outra variável, ou com qualquer constante, função ou expressão de predicados.