–RESOLUÇÃO NA LÓGICA PROPOSICIONAL
–EXEMPLO: P, (P ^ Q) ®
R, S v T ® Q , T\ R
•Primeiro convertemos os axiomas em cláusulas.
•1. P
•2. Ø P v Ø Q v R
•3. Ø S v Q
•4. Ø T v Q
•5. T
•6. Ø R
•Começamos então a escolher a par de cláusulas para resolver. Embora
qualquer par de cláusulas
possa ser resolvido, apenas
aqueles pares que contenham literais complementares produzirão um resolvente com possibilidade de
produzir uma cláusula
vazia.
•Começamos por resolver com a cláusula
ØR, pois ela é uma das cláusulas que deverão estar envolvidas na
contradição que
estamos tentando encontrar.
•1. P
•2. Ø P v Ø Q v R
•3. Ø S v Q
•4. Ø T v Q
•5. T
•6. Ø R
•------------------------------------------
•7. Ø P v Ø Q (2
e 6)
•8. Ø Q (1
e 7)
•9. Ø T (4 e
8)
•10. VAZIA (5
e 9)
•
•