–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)  
•
•