Esercizio - Conversione in CNF e risoluzione proposizionale (slide del corso)

Testo (dalle slide "Logical agents" del corso di Intelligenza Artificiale, Ing. dell'Informazione UniPD, esempio del mondo del Wumpus; teoria in Agenti logici e logica proposizionale - inferenza e risoluzione).

Convertire in CNF $R_3: B_{2,1} \Leftrightarrow (P_{1,1} \lor P_{2,2} \lor P_{3,1})$ .
L'agente è passato da $[1,1]$ (nessun pozzo, $R_1: \neg P_{1,1}$ ) a $[2,1]$ , dove sente brezza ( $R_5: B_{2,1}$ ), e poi in $[1,2]$ dove non sente brezza ( $\neg B_{1,2}$ ). La regola di $[1,2]$ è $R_6: B_{1,2} \Leftrightarrow (P_{1,1} \lor P_{2,2} \lor P_{1,3})$ . Dimostrare per risoluzione che c'è un pozzo in $[3,1]$ , cioè $KB' \models P_{3,1}$ , con $KB' = R_1 \land R_3 \land R_5 \land R_6 \land \neg B_{1,2}$ . Dimostrare anche che $\neg P_{2,2}$ segue.

Punto 1: CNF di $R_3$

Si applicano i passi della nota.

Eliminare $\Leftrightarrow$ : $\alpha \Leftrightarrow \beta$ diventa $(\alpha \Rightarrow \beta) \land (\beta \Rightarrow \alpha)$ con $\alpha = B_{2,1}$ e $\beta = P_{1,1} \lor P_{2,2} \lor P_{3,1}$ : $(B_{2,1} \Rightarrow (P_{1,1} \lor P_{2,2} \lor P_{3,1})) \land ((P_{1,1} \lor P_{2,2} \lor P_{3,1}) \Rightarrow B_{2,1}).$
Eliminare $\Rightarrow$ ( $\alpha \Rightarrow \beta \equiv \neg\alpha \lor \beta$ ): $(\neg B_{2,1} \lor P_{1,1} \lor P_{2,2} \lor P_{3,1}) \land (\neg(P_{1,1} \lor P_{2,2} \lor P_{3,1}) \lor B_{2,1}).$
De Morgan: $\neg(P_{1,1} \lor P_{2,2} \lor P_{3,1}) = \neg P_{1,1} \land \neg P_{2,2} \land \neg P_{3,1}$ : $(\neg B_{2,1} \lor P_{1,1} \lor P_{2,2} \lor P_{3,1}) \land ((\neg P_{1,1} \land \neg P_{2,2} \land \neg P_{3,1}) \lor B_{2,1}).$
Distribuire $\lor$ su $\land$ : $(a \land b \land c) \lor d = (a \lor d) \land (b \lor d) \land (c \lor d)$ con $d = B_{2,1}$ : $(\neg B_{2,1} \lor P_{1,1} \lor P_{2,2} \lor P_{3,1}) \land (\neg P_{1,1} \lor B_{2,1}) \land (\neg P_{2,2} \lor B_{2,1}) \land (\neg P_{3,1} \lor B_{2,1}).$

Risultato: quattro clausole (una lunga più una per ogni pozzo adiacente: "un pozzo adiacente implica brezza"). Il controllo con sympy (to_cnf) dà le stesse quattro clausole. Con la stessa tecnica $R_6$ dà $(\neg B_{1,2} \lor P_{1,1} \lor P_{2,2} \lor P_{1,3}) \land (\neg P_{1,1} \lor B_{1,2}) \land (\neg P_{2,2} \lor B_{1,2}) \land (\neg P_{1,3} \lor B_{1,2})$ .

Punto 2: $KB' \models P_{3,1}$

Clausole.

	clausola	origine
$c_1$	$\neg P_{1,1}$	$R_1$
$c_2$	$B_{2,1}$	$R_5$
$c_3$	$\neg B_{2,1} \lor P_{1,1} \lor P_{2,2} \lor P_{3,1}$	$R_3$ (clausola lunga)
$c_4$	$\neg B_{1,2}$	percezione
$c_5$	$\neg P_{2,2} \lor B_{1,2}$	$R_6$ (da $P_{2,2} \Rightarrow B_{1,2}$ )
$c_6$	$\neg P_{3,1}$	negazione della tesi $\neg\alpha$

(Delle altre clausole di $R_3$ e $R_6$ non serve nessuna: nella risoluzione si usano solo quelle necessarie.)

Derivazione.

$c_2$ e $c_3$ su $B_{2,1}$ : $s_1 = P_{1,1} \lor P_{2,2} \lor P_{3,1}$ .
$s_1$ e $c_1$ su $P_{1,1}$ : $s_2 = P_{2,2} \lor P_{3,1}$ (almeno uno tra $[2,2]$ e $[3,1]$ ha il pozzo).
$s_2$ e $c_6$ su $P_{3,1}$ : $s_3 = P_{2,2}$ .
$s_3$ e $c_5$ su $P_{2,2}$ : $s_4 = B_{1,2}$ .
$s_4$ e $c_4$ su $B_{1,2}$ : $\square$ .

La clausola vuota mostra che $KB' \land \neg P_{3,1}$ è insoddisfacibile: $KB' \models P_{3,1}$ , c'è un pozzo in $[3,1]$ .

$\neg P_{2,2}$ . Si aggiunge la negazione, $P_{2,2}$ . Con $c_5$ su $P_{2,2}$ : $B_{1,2}$ ; con $c_4$ su $B_{1,2}$ : $\square$ . Quindi $KB' \models \neg P_{2,2}$ . Con $\neg P_{2,2}$ in mano, il passo 2 ( $s_2 = P_{2,2} \lor P_{3,1}$ ) dà direttamente $P_{3,1}$ : è lo stesso ragionamento della slide "Exploring a wumpus world".

Controllo con Python. Un risolutore a saturazione sulle clausole conferma: $KB' \land \neg P_{3,1}$ è refutabile, $KB' \land P_{3,1}$ no; $KB' \land P_{2,2}$ e $KB' \land P_{1,3}$ sono refutabili. Per model checking sui $6$ simboli $B_{2,1}, B_{1,2}, P_{1,1}, P_{2,2}, P_{3,1}, P_{1,3}$ ( $2^6 = 64$ modelli) la KB ha un solo modello: $P_{3,1}$ vero e tutti gli altri falsi tranne $B_{2,1}$ . Rispetto ai $3$ modelli della nota, il nuovo dato $\neg B_{1,2}$ ha eliminato $P_{2,2}$ e quindi l'ambiguità.

Versione ripasso

CNF di $R_3$ : $B_{2,1} \Leftrightarrow (P_{1,1} \lor P_{2,2} \lor P_{3,1})$ . Eliminare $\Leftrightarrow$ e $\Rightarrow$ , De Morgan sul $\neg(\dots)$ , distribuire. Risultato: $(\neg B_{2,1} \lor P_{1,1} \lor P_{2,2} \lor P_{3,1}) \land (\neg P_{1,1} \lor B_{2,1}) \land (\neg P_{2,2} \lor B_{2,1}) \land (\neg P_{3,1} \lor B_{2,1})$ . $R_6$ analogo con $B_{1,2}$ , $P_{1,3}$ .
Dati: $c_1 = \neg P_{1,1}$ , $c_2 = B_{2,1}$ , $c_3$ = clausola lunga di $R_3$ , $c_4 = \neg B_{1,2}$ , $c_5 = \neg P_{2,2} \lor B_{1,2}$ , $c_6 = \neg P_{3,1}$ ( $\neg\alpha$ ).
Prova di $P_{3,1}$ : $c_2, c_3 \to P_{1,1} \lor P_{2,2} \lor P_{3,1}$ ; con $c_1 \to P_{2,2} \lor P_{3,1}$ ; con $c_6 \to P_{2,2}$ ; con $c_5 \to B_{1,2}$ ; con $c_4 \to \square$ . Prova di $\neg P_{2,2}$ : $P_{2,2}$ con $c_5 \to B_{1,2}$ , con $c_4 \to \square$ .
Verifica: model checking su $6$ simboli, $64$ modelli: ne resta uno ( $P_{3,1}$ vero). Il dato $\neg B_{1,2}$ passa da $3$ modelli a $1$ .
Errore tipico: dimenticare di aggiungere $\neg\alpha$ , oppure risolvere su due letterali complementari insieme (si risolve su un letterale per volta).

Esercizi su questo argomento

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

Teoria collegata

Agenti logici e logica proposizionale - inferenza e risoluzione