Una tavola di verità dice se una formula è una tautologia, ma con molte variabili diventa ingestibile. C'è un altro modo di ragionare: partire da premesse note e ricavare nuove conclusioni con passaggi semplici, ciascuno dei quali è garantito corretto. Questi passaggi si chiamano regole di inferenza, e sono la grammatica di ogni dimostrazione, dalla matematica ai sistemi di verifica automatica.
Che cosa rende valida un'inferenza
Un'inferenza è valida quando è impossibile che le premesse siano tutte vere e la conclusione falsa. In termini formali: se le premesse sono P₁, …, Pₙ e la conclusione è C, l'inferenza è valida se (P₁ ∧ … ∧ Pₙ) → C è una tautologia.
Validità e verità sono cose diverse. Un ragionamento valido con una premessa falsa può portare a una conclusione falsa; un ragionamento non valido può arrivare per caso a una conclusione vera. La validità riguarda solo la forma.
Le regole principali
| Regola | Premesse | Conclusione |
|---|---|---|
| Modus ponens | p → q, p | q |
| Modus tollens | p → q, ¬q | ¬p |
| Sillogismo ipotetico | p → q, q → r | p → r |
| Sillogismo disgiuntivo | p ∨ q, ¬p | q |
| Addizione | p | p ∨ q |
| Semplificazione | p ∧ q | p |
| Congiunzione | p, q | p ∧ q |
| Risoluzione | p ∨ q, ¬p ∨ r | q ∨ r |
Vediamo il senso di alcune.
Modus ponens
È la regola più naturale: se vale «se p allora q» e vale p, allora vale q. «Se il certificato è scaduto, il browser mostra un avviso. Il certificato è scaduto. Quindi il browser mostra un avviso.»
Modus tollens
Si ragiona all'indietro dalla conclusione negata: «se il disco è pieno, il log riporta un errore di scrittura. Il log non riporta errori di scrittura. Quindi il disco non è pieno.» È la regola che si usa per escludere ipotesi durante una diagnosi.
Sillogismo disgiuntivo
Se una tra due alternative deve valere e una è esclusa, resta l'altra. «Il guasto è nel client o nel server. Il client funziona con un altro server. Quindi il guasto è nel server.» Attenzione: funziona solo se la disgiunzione di partenza è davvero completa.
Risoluzione
È la regola meno intuitiva, ma la più potente per le macchine. Se in una clausola compare p e in un'altra ¬p, si possono unire le due eliminando la coppia. Da «p ∨ q» e «¬p ∨ r» si ricava «q ∨ r»: se p è vero, allora r deve esserlo per la seconda clausola; se p è falso, q deve esserlo per la prima. In ogni caso vale q ∨ r.
Un esempio di deduzione formale
Premesse:
- Se il backup notturno è riuscito, allora il file di stato esiste. (b → f)
- Se il file di stato esiste, allora il monitoraggio è verde. (f → m)
- Il monitoraggio non è verde. (¬m)
- Il backup notturno è riuscito oppure è partito l'allarme. (b ∨ a)
Vogliamo dimostrare che è partito l'allarme (a).
| Passo | Formula | Giustificazione |
|---|---|---|
| 5 | b → m | sillogismo ipotetico da 1 e 2 |
| 6 | ¬b | modus tollens da 5 e 3 |
| 7 | a | sillogismo disgiuntivo da 4 e 6 |
Tre passaggi, ognuno dei quali applica una sola regola. Questo è lo stile di una dimostrazione formale: niente salti, ogni riga giustificata da regole e righe precedenti.
Dimostrare per refutazione con la risoluzione
I dimostratori automatici usano spesso un approccio diverso: aggiungono alle premesse la negazione della tesi e cercano di ottenere una contraddizione, cioè la clausola vuota. Se ci riescono, la tesi segue dalle premesse.
Rifacciamo l'esempio in questo modo. Trasformiamo tutto in clausole: ¬b ∨ f, ¬f ∨ m, ¬m, b ∨ a, e la negazione della tesi ¬a.
- Da b ∨ a e ¬a: b.
- Da ¬b ∨ f e b: f.
- Da ¬f ∨ m e f: m.
- Da m e ¬m: clausola vuota.
Contraddizione raggiunta, quindi a è dimostrata. Il vantaggio è che la macchina ha bisogno di una sola regola, applicata ripetutamente. È l'idea su cui si basano il linguaggio Prolog e molti strumenti di verifica.
Errori da riconoscere
Due schemi sembrano regole ma non lo sono:
- Affermazione del conseguente: da p → q e q concludere p.
- Negazione dell'antecedente: da p → q e ¬p concludere ¬q.
Un controllo veloce: se avete un dubbio su uno schema, cercate un'assegnazione che renda vere le premesse e falsa la conclusione. Se la trovate, lo schema non è valido. Per l'affermazione del conseguente basta p falso e q vero.
In sintesi
- Un'inferenza è valida se premesse vere non possono portare a una conclusione falsa; conta solo la forma.
- Modus ponens, modus tollens e i sillogismi coprono la gran parte dei ragionamenti quotidiani.
- Una dimostrazione formale è una sequenza di righe, ciascuna giustificata da una regola.
- La risoluzione, unita alla refutazione, permette alle macchine di dimostrare con una sola regola.
- Per smascherare uno schema non valido basta trovare un controesempio.
