Esercizio - Risoluzione, forward e backward chaining sul caso Criminal West (slide del corso)

In questa pagina 5

Testo (dalle slide "Inference in first-order logic" del corso di Intelligenza Artificiale, Ing. dell'Informazione UniPD; teoria in Logica del primo ordine - unificazione, forward e backward chaining). La legge dice che è un reato per un americano vendere armi a nazioni ostili. Il paese Nono, nemico dell'America, ha dei missili, e tutti i suoi missili gli sono stati venduti dal colonnello West, che è americano.

Tradurre il testo in logica del primo ordine, con le convenzioni che un nemico dell'America è ostile e che un missile è un'arma.
Dimostrare $Criminal(West)$ per risoluzione, per backward chaining e per forward chaining.
Cosa succede se si toglie un fatto alla volta? Quale risposta dà la domanda $Criminal(x)$ ?

Punto 1: formalizzazione

Frase	Logica
reato vendere armi a nazioni ostili	$American(x) \land Weapon(y) \land Sells(x,y,z) \land Hostile(z) \Rightarrow Criminal(x)$
Nono è nemica dell'America	$Enemy(Nono, America)$
un nemico dell'America è ostile	$Enemy(x, America) \Rightarrow Hostile(x)$
Nono ha dei missili	$\exists x\ Owns(Nono,x) \land Missile(x)$ , con EI: $Owns(Nono,M_1)$ e $Missile(M_1)$
i missili sono armi	$Missile(x) \Rightarrow Weapon(x)$
West ha venduto a Nono tutti i missili di Nono	$Missile(x) \land Owns(Nono,x) \Rightarrow Sells(West,x,Nono)$
West è americano	$American(West)$

L'esistenziale è eliminato con la costante di Skolem $M_1$ (nome nuovo). Le variabili sono quantificate universalmente. Sono tutte clausole definite: un solo letterale positivo per clausola, quindi vanno bene sia forward sia backward chaining.

Punto 2a: risoluzione

Negazione della tesi: $\neg Criminal(West)$ . Nove passi, riportati con le sostituzioni, nella nota; in sintesi: $\neg Criminal(West)$ con la regola del reato ( $x/West$ ), poi $American(West)$ , la regola $Missile \Rightarrow Weapon$ ( $x/y$ ), $Missile(M_1)$ ( $y/M_1$ ), la regola delle vendite ( $x/M_1$ , $z/Nono$ ), ancora $Missile(M_1)$ , $Owns(Nono,M_1)$ , la regola dei nemici ( $x/Nono$ ) e $Enemy(Nono,America)$ , che dà $\square$ . La clausola vuota prova $Criminal(West)$ .

Punto 2b: backward chaining

Si parte da $Criminal(West)$ e si cercano clausole la cui conseguenza si unifica con l'obiettivo. Le variabili della regola sono rinominate a ogni uso (apice). In profondità, da sinistra a destra:

Obiettivo $Criminal(West)$ : la regola del reato ha conseguenza $Criminal(x)$ , con $\{x/West\}$ . Nuovi obiettivi (premesse): $American(West)$ , $Weapon(y)$ , $Sells(West,y,z)$ , $Hostile(z)$ .
$American(West)$ : è un fatto. $\{\}$ .
$Weapon(y)$ : la regola $Missile(x') \Rightarrow Weapon(x')$ dà $\{y/x'\}$ e obiettivo $Missile(x')$ ; il fatto $Missile(M_1)$ dà $\{x'/M_1\}$ , cioè $y = M_1$ .
$Sells(West,M_1,z)$ : la regola $Missile(x'') \land Owns(Nono,x'') \Rightarrow Sells(West,x'',Nono)$ si unifica con $\{z/Nono,\ x''/M_1\}$ . Obiettivi: $Missile(M_1)$ (fatto) e $Owns(Nono,M_1)$ (fatto).
$Hostile(Nono)$ (con $z = Nono$ ): la regola $Enemy(x''', America) \Rightarrow Hostile(x''')$ dà $\{x'''/Nono\}$ ; obiettivo $Enemy(Nono, America)$ , fatto.

Tutte le foglie sono fatti: $Criminal(West)$ è dimostrato con $\{x/West, y/M_1, z/Nono\}$ . Un solo ramo, nessun vicolo cieco: ogni obiettivo ha una sola clausola che si unifica (il programma Python di verifica trova la risposta senza tornare indietro su nessuna scelta).

Punto 2c: forward chaining

Si applicano le regole le cui premesse sono già tutte fatti, finché non compare nulla di nuovo.

Giro	Regola	Sostituzione	Fatto nuovo
1	$Missile(x) \Rightarrow Weapon(x)$	$\{x/M_1\}$	$Weapon(M_1)$
1	$Missile(x) \land Owns(Nono,x) \Rightarrow Sells(West,x,Nono)$	$\{x/M_1\}$	$Sells(West,M_1,Nono)$
1	$Enemy(x,America) \Rightarrow Hostile(x)$	$\{x/Nono\}$	$Hostile(Nono)$
2	$American(x) \land Weapon(y) \land Sells(x,y,z) \land Hostile(z) \Rightarrow Criminal(x)$	$\{x/West, y/M_1, z/Nono\}$	$Criminal(West)$
3	nessuna regola dà qualcosa di nuovo		punto fisso

La regola del reato non poteva scattare al giro 1: mancavano $Weapon$ , $Sells$ e $Hostile$ . Per questo servono due giri. Al punto fisso i fatti sono $8$ (i $4$ iniziali più $4$ derivati).

Punto 3: togliere un fatto, domanda $Criminal(x)$

Si rifanno forward e backward chaining togliendo un fatto alla volta (controllo con Python). In ogni caso $Criminal(West)$ non si deriva, sia con forward sia con backward chaining:

Fatto tolto	Cosa manca	Fatti derivati dal forward
$Owns(Nono,M_1)$	non si può provare $Sells(West,M_1,Nono)$	$Weapon(M_1)$ , $Hostile(Nono)$
$Enemy(Nono,America)$	non si può provare $Hostile(Nono)$	$Weapon(M_1)$ , $Sells(West,M_1,Nono)$
$American(West)$	manca la prima premessa	$Weapon(M_1)$ , $Sells(West,M_1,Nono)$ , $Hostile(Nono)$
$Missile(M_1)$	manca l'arma, e anche la vendita	solo $Hostile(Nono)$

È il debug della KB: togliere o cambiare un enunciato e vedere quale conclusione cade. Se la KB è completa per il problema, ogni fatto è necessario.

Domanda con variabile. Ask(KB, Criminal(x)): il backward chaining, con la stessa catena di prima, restituisce la sostituzione $\{x/West\}$ (e le altre variabili legate, $y = M_1$ e $z = Nono$ , non fanno parte della risposta). È l'unico criminale derivabile.

Versione ripasso

Formalizzazione (clausole definite): $American(x) \land Weapon(y) \land Sells(x,y,z) \land Hostile(z) \Rightarrow Criminal(x)$ ; $Enemy(Nono,America)$ ; $Enemy(x,America) \Rightarrow Hostile(x)$ ; EI su "ha missili": $Owns(Nono,M_1)$ , $Missile(M_1)$ ; $Missile(x) \Rightarrow Weapon(x)$ ; $Missile(x) \land Owns(Nono,x) \Rightarrow Sells(West,x,Nono)$ ; $American(West)$ .
Risoluzione: negare la tesi, $\neg Criminal(West)$ ; sequenza regola del reato ( $x/West$ ), $American(West)$ , $Missile \Rightarrow Weapon$ ( $x/y$ ), $Missile(M_1)$ ( $y/M_1$ ), regola vendite ( $x/M_1$ , $z/Nono$ ), $Missile(M_1)$ , $Owns(Nono,M_1)$ , regola nemici ( $x/Nono$ ), $Enemy(Nono,America)$ : $\square$ in $9$ passi.
Backward chaining (in profondità): $Criminal(West)$ con $\{x/West\}$ ; premesse $American(West)$ (fatto), $Weapon(y)$ via $Missile$ con $y/M_1$ , $Sells(West,M_1,z)$ con $\{z/Nono\}$ (premesse $Missile(M_1)$ , $Owns(Nono,M_1)$ ), $Hostile(Nono)$ via $Enemy(Nono,America)$ . Risultato $\{x/West, y/M_1, z/Nono\}$ , nessun ritorno indietro.
Forward chaining: giro 1 $Weapon(M_1)$ , $Sells(West,M_1,Nono)$ , $Hostile(Nono)$ ; giro 2 $Criminal(West)$ ; giro 3 punto fisso; $8$ fatti in tutto.
Debug: senza $Owns(Nono,M_1)$ , $Enemy(Nono,America)$ , $American(West)$ o $Missile(M_1)$ , $Criminal(West)$ non si deriva. Ask(KB, Criminal(x)) dà $\{x/West\}$ .
Errore tipico: dimenticare di rinominare le variabili a ogni uso della regola, o di propagare la sostituzione (es. $z/Nono$ ) alle premesse successive.

Teoria collegata

Logica del primo ordine - unificazione, forward e backward chaining