–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.