Anzitutto va precisato che è più corretto parlare di risoluzione di una clausola, piuttosto che dimostrazione di una clausola.
Ricordiamo che una clausola è disgiunzione di letterali: i congiunti che compongono una FNC (forma normale congiuntiva) vengono separati, ed ognuno di essi diventa una fbf (formula ben formata).
La fondamentale regola di risoluzione delle clausole è data quando sono presenti due clausole che contengono una stessa variabile, diciamo P, che risulta affermata in una e negata nell’altra. Dunque sono date
Tale regola di inferenza è valida anche nel caso
Vediamo un esempio di applicazione: ci proponiamo di risolvere il sistema fomato dalle seguenti clausole:
1. P∨Q∨R
2. (nonP)∨Q∨R
3. P∨(nonQ)∨R
4. P∨Q∨(nonR)
5. (nonP)∨(nonQ)∨R
6.(nonP)∨Q∨(nonR)
7. P∨(nonQ)∨(nonR)
8.(nonP)∨(nonQ)∨(nonR).
Cominciamo col risolvere 1-2; otteniamo, per la regola di inferenza
9. Q∨R
Risolviamo 3-5; si ha
10. (nonQ)∨R.
Risolviamo 4-6; si ha
11. Q∨(nonR).
Risolviamo 7-8; si ha
12. (nonQ)∨(nonR).
Risolviamo 9-10; si ha
13. R.
Risolviamo 11-12; si ha
14. nonR.
Risolviamo 13-14; si ha
15. [ ].
Abbiamo ottenuto la clausola vuota; il sistema 1–8 è dunque contradditorio (si verifica con le tavole di verità.)
Si può verificare che togliendo la clausola 8, il sistema 1–7 diventa non contradditorio, e più precisamente si risolve in Q.
In generale valgono i due Teoremi:
Teorema di plausibilità: Se risolvendo un insieme di clausole si ottiene la clausola vuota, allora il sistema di partenza è contradditorio.
Teorema di completezza: Se un insieme di clausole è contradditorio, risolvendolo otteniamo la clausola vuota.