Salve, la mia domanda riguarda la logica e in particolare le clausole.Vorrei sapere come si dimostra una clausola.

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

H∨P (nonP)∨K

La regola di risoluzione afferma che in tali condizioni si può asserire H∨K. Infatti se H∨P e (nonP)∨K sono entrambe vere, ciò implica che o H (nel caso P falsa) o K (nel caso P vera) sarà vera (è sicuramente falsa o P o (nonP)). Dunque è sicuramente vera H∨K.
Tale regola di inferenza è valida anche nel caso

P nonP

ed ha come risoluzione la clausola vuota, spesso denotata con [ ].

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.