–RESOLUÇÃO NA LÓGICA DOS PREDICADOS
–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.
–ALGORITMO
–1. Converter todas as declarações de F em cláusulas.
–2. Negar S e converter o resultado em cláusulas. Acrescentá-las ao conjunto de cláusulas obtidas em 1.
–3. Repetir até que uma contradição seja encontrada, e nenhum progresso possa ser feito, ou até que se tenha gasto um quantidade pré-determinada de esforço:
•3.1. Escolher duas cláusulas e chamá-las de cláusulas pais.
•3.2. Resolvê-las. O resolvente será a disjunção de todos os literais de ambas as cláusulas pais com as substituições apropriadas realizadas, ressalvando-se o seguinte:
–3.2.1. Se houver um par de literais T1 e Ø T2 tal que uma das cláusulas pais contenha T1 e a outra contenha T2, e ainda se T1 e T2 forem unificáveis, então nem T1 nem T2 devem aparecer no resolvente.
–3.2.2. Chamaremos T1 e T2 literais complementares. Utilize a substituição produzida pela unificação para criar o resolvente.