Esercizio - Forma normale congiuntiva dell'equivalenza con una disgiunzione (esempio d'esame 2)

Teoria: Agenti logici e logica proposizionale - inferenza e risoluzioneAgenti basati sulla conoscenza (KB, Tell e Ask), mondo del Wumpus come banco di prova, sintassi e semantica della logica proposizionale, conseguenza logica, equivalenze, inferenza per model checking (7 simboli, 128 modelli, 3 modelli della KB) e per risoluzione (CNF, regola di risoluzione, dimostrazione per assurdo). Limite: poca espressività, da cui la logica del primo ordine.Agenti logici e logica proposizionale - inferenza e risoluzione → (sezione sulla forma normale congiuntiva e tabella delle equivalenze). Esercizio collegato: Esercizio - Conversione in CNF e risoluzione proposizionale (slide del corso). Domanda 1 del quiz da 9 CFU (la logica non è nel programma da 6 CFU).

Testo. Indicare la corretta forma normale congiuntiva (CNF) della formula $A\Leftrightarrow(B\lor C)$. Menu, cinque opzioni:

1. $(A\lor\neg B)\land(B\lor\neg C)$
2. $(A\Rightarrow(B\lor C))\land((B\lor C)\Rightarrow A)$
3. $\neg A\land(\neg B\lor A)\land(\neg C\lor A)$
4. Nessuna delle opzioni
5. $(\neg A\lor B\lor C)\land(\neg B\lor A)\land(\neg C\lor A)$

Soluzione

La CNF è una congiunzione di clausole, ciascuna disgiunzione di letterali. Passi:

1. Eliminazione della doppia implicazione: $A\Leftrightarrow(B\lor C)\equiv(A\Rightarrow(B\lor C))\land((B\lor C)\Rightarrow A)$ (è la forma dell'opzione 2).
2. Eliminazione dell'implicazione, $\alpha\Rightarrow\beta\equiv\neg\alpha\lor\beta$:

• $A\Rightarrow(B\lor C)\equiv\neg A\lor B\lor C$ (già una clausola);
• $(B\lor C)\Rightarrow A\equiv\neg(B\lor C)\lor A$.

3. De Morgan: $\neg(B\lor C)\equiv\neg B\land\neg C$, quindi $(\neg B\land\neg C)\lor A$.
4. Distributività di $\lor$ su $\land$: $(\neg B\land\neg C)\lor A\equiv(\neg B\lor A)\land(\neg C\lor A)$.

Insieme: $(\neg A\lor B\lor C)\land(\neg B\lor A)\land(\neg C\lor A)$. Risposta: opzione 5. Tre clausole: $\{\neg A,B,C\}$, $\{\neg B,A\}$, $\{\neg C,A\}$.

Perché le altre sono sbagliate

La tabella di verità (verificata con Python) confronta la formula con le opzioni 1, 3 e 5; l'opzione 5 coincide in tutte le righe, le altre no.

• Opzione 1: sbaglia due righe. Per $A=V,B=F,C=F$ la formula è falsa ($A$ vero ma $B\lor C$ falso) e l'opzione dà vero: manca la clausola $\neg A\lor B\lor C$ (la direzione $A\Rightarrow B\lor C$). Per $A=V,B=F,C=V$ la formula è vera e l'opzione dà falso: la clausola $B\lor\neg C$ pretende $B$ vero quando $C$ è vero, ma dalla formula segue solo che $C$ vero implica $A$ vero.
• Opzione 2: equivalente alla formula, ma non è in CNF: contiene implicazioni invece di disgiunzioni di letterali (è solo il primo passo).
• Opzione 3: la clausola $\neg A$ da sola forza $A$ falso: l'opzione è falsa in tutte le righe con $A=V$, comprese tre in cui la formula è vera. Errore tipico: distribuire in modo scorretto.
• Opzione 4: non vale, perché l'opzione 5 è corretta.