–ALGORITMO
•3.3. Se o resolvente for uma cláusula
vazia, então foi
encontrada uma contradição. Se não for, acrescente-o ao conjunto de cláusulas disponíveis para o
procedimento.
–Se
a escolha de cláusulas a resolver em cada passo for feita de maneira sistemática, o procedimento de
resolução encontrará
uma contradição, se ela existir.
–EXEMPLO:
–Homem(Marco)
–Pompeiano(Marco)
–"x Pompeiano(x) ®
Romano(x)
–Soberano(Cesar)
–"x Romano(x) ®
(LealA(x,Cesar) v Odiar(x,Cesar))
–"x$y LealA(x,y)
–"x"y (Homem(x) ^ Soberano(y)) v (TentarAssassinar(x,y) ^
LealA(x,y))
–TentarAssassinar(Marco,Cesar)
–Logo,
Odiar(Marco, Cesar)
•Primeiro convertemos os axiomas em
cláusulas.
–1. Homem(Marco)
–2. Pompeiano(Marco)
–3. Ø Pompeiano(x1) v Romano(x1)
–4. Soberano(Cesar)
–5. Ø Romano(x2) v LealA(x2,Cesar) v Odiar(x2,Cesar)
–6. LealA(x3,f1(x3)
–7. Ø Homem(x4) v Ø
Soberano(y1) v Ø TentarAssassinar(x4,y1) v Ø LealA(x4,y1)
–8. TentarAssassinar(Marco,Cesar)
–9. Ø Odiar(Marco,Cesar)