Esercizio - Unificazione e conversione in CNF nel primo ordine (slide del corso)

In questa pagina 3

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).

Unificare le coppie della tabella delle slide: $Knows(John, x)$ con $Knows(John, Jane)$ , con $Knows(y, Mary)$ , con $Knows(y, Mother(y))$ , con $Knows(x, Mary)$ .
Altre coppie: $P(x, f(y))$ e $P(g(z), z)$ ; $Q(x,x)$ e $Q(A,B)$ ; $Q(x,y)$ e $Q(y,A)$ ; $R(x, f(x))$ e $R(y,y)$ .
Convertire in CNF: (a) "chi ama tutti gli animali è amato da qualcuno" (esempio delle slide); (b) "chi possiede un cane è un amante degli animali"; (c) "ogni studente ha superato qualche esame".

Punto 1: la tabella delle slide

Convenzione: le variabili sono minuscole, le costanti maiuscole. Si legano le variabili confrontando gli argomenti da sinistra a destra; dopo ogni legame lo si applica ai termini seguenti.

$\alpha$	$\beta$	Passi	$\theta$
$Knows(John,x)$	$Knows(John,Jane)$	$John = John$ ok; $x$ con $Jane$ : $x/Jane$	$\{x/Jane\}$
$Knows(John,x)$	$Knows(y,Mary)$	$John$ con $y$ : $y/John$ ; $x$ con $Mary$ : $x/Mary$	$\{y/John,\ x/Mary\}$
$Knows(John,x)$	$Knows(y,Mother(y))$	$y/John$ ; poi $x$ con $Mother(y)$ , che con $y = John$ è $Mother(John)$	$\{y/John,\ x/Mother(John)\}$
$Knows(John,x)$	$Knows(x,Mary)$	$John$ con $x$ : $x/John$ ; poi $x$ (cioè $John$ ) con $Mary$ : due costanti diverse	fallisce

L'ultimo fallimento dipende solo dal nome: i due $x$ appartengono a enunciati diversi. Standardizzando il secondo ( $z$ al posto di $x$ ) si ha $Knows(John,x)$ con $Knows(z,Mary)$ : $z/John$ , $x/Mary$ e $\theta = \{x/Mary,\ z/John\}$ .

Punto 2: altre coppie

$P(x,f(y))$ e $P(g(z),z)$ : primo argomento $x$ con $g(z)$ : $x/g(z)$ . Secondo: $f(y)$ con $z$ : $z/f(y)$ . Applicando $z/f(y)$ anche a $x$ : $\theta = \{z/f(y),\ x/g(f(y))\}$ . Entrambi diventano $P(g(f(y)), f(y))$ .
$Q(x,x)$ e $Q(A,B)$ : $x/A$ ; secondo argomento: $x$ (cioè $A$ ) contro $B$ : costanti diverse, fallisce.
$Q(x,y)$ e $Q(y,A)$ : $x/y$ ; secondo argomento: $y$ con $A$ : $y/A$ ; applicando $y/A$ anche a $x$ : $\theta = \{y/A,\ x/A\}$ . Entrambi diventano $Q(A,A)$ .
$R(x,f(x))$ e $R(y,y)$ : $x/y$ ; secondo argomento: $f(x)$ , cioè $f(y)$ , contro $y$ : $y$ compare in $f(y)$ , quindi l'occur check blocca il legame: fallisce. Senza il controllo si legherebbe $y/f(y)$ , un termine infinito.

Controllati con la funzione unify della nota: restituisce i legami elencati e None nei tre casi di fallimento.

Punto 3: conversione in CNF

(a) Animali. $\forall x\ [\forall y\ Animal(y) \Rightarrow Loves(x,y)] \Rightarrow [\exists y\ Loves(y,x)]$ .

Eliminare $\Rightarrow$ ( $A \Rightarrow B \equiv \neg A \lor B$ ), prima l'implicazione interna e poi l'esterna: $\forall x\ \neg[\forall y\ (\neg Animal(y) \lor Loves(x,y))] \lor [\exists y\ Loves(y,x)]$ .
Portare $\neg$ dentro: $\neg\forall y\ p \equiv \exists y\ \neg p$ , poi De Morgan e doppia negazione: $\forall x\ [\exists y\ Animal(y) \land \neg Loves(x,y)] \lor [\exists y\ Loves(y,x)]$ .
Standardizzare le due $y$ (sono variabili diverse): $\forall x\ [\exists y\ Animal(y) \land \neg Loves(x,y)] \lor [\exists z\ Loves(z,x)]$ .
Skolemizzare: entrambi gli $\exists$ sono sotto $\forall x$ , quindi funzioni di $x$ : $y \to F(x)$ , $z \to G(x)$ : $\forall x\ [Animal(F(x)) \land \neg Loves(x,F(x))] \lor Loves(G(x),x)$ .
Togliere $\forall x$ .
Distribuire: $(a \land b) \lor c = (a \lor c) \land (b \lor c)$ : $[Animal(F(x)) \lor Loves(G(x),x)] \land [\neg Loves(x,F(x)) \lor Loves(G(x),x)].$

Verifica numerica: su un dominio di $3$ oggetti, per tutte le $2^3 \cdot 2^9 = 4096$ interpretazioni di $Animal$ e $Loves$ , l'enunciato originale è vero se e solo se esiste una scelta delle funzioni $F, G$ (tra le $27 \cdot 27$ ) che rende vera la CNF. Zero discordanze.

(b) Cani. $\forall x\ (\exists y\ Dog(y) \land Owns(x,y)) \Rightarrow AnimalLover(x)$ .

Eliminare $\Rightarrow$ : $\forall x\ \neg(\exists y\ Dog(y) \land Owns(x,y)) \lor AnimalLover(x)$ .
Portare $\neg$ dentro: $\neg\exists y\ p \equiv \forall y\ \neg p$ e De Morgan: $\forall x\ (\forall y\ \neg Dog(y) \lor \neg Owns(x,y)) \lor AnimalLover(x)$ .
Nessun $\exists$ rimasto: niente Skolem. Togliere i $\forall$ : $\neg Dog(y) \lor \neg Owns(x,y) \lor AnimalLover(x)$ .

Una clausola. L' $\exists$ nell'antecedente è diventato $\forall$ : "se esiste un cane posseduto allora" è lo stesso che "per ogni cane posseduto".

(c) Esami. $\forall x\ Student(x) \Rightarrow \exists y\ Exam(y) \land Passed(x,y)$ .

$\forall x\ \neg Student(x) \lor \exists y\ (Exam(y) \land Passed(x,y))$ .
Skolem: $y \to F(x)$ (l'esame dipende dallo studente): $\neg Student(x) \lor (Exam(F(x)) \land Passed(x,F(x)))$ . Con una costante invece di $F(x)$ si direbbe che tutti hanno superato lo stesso esame.
Distribuire: $[\neg Student(x) \lor Exam(F(x))] \land [\neg Student(x) \lor Passed(x, F(x))]$ .

Due clausole.

Versione ripasso

Unificazione (variabili minuscole, da sinistra, applicando i legami già fatti): $Knows(John,x)$ con $Knows(John,Jane)$ dà $\{x/Jane\}$ ; con $Knows(y,Mary)$ dà $\{x/Mary, y/John\}$ ; con $Knows(y,Mother(y))$ dà $\{y/John, x/Mother(John)\}$ ; con $Knows(x,Mary)$ fallisce (stesso nome $x$ ), ma standardizzando $z$ si ha $\{x/Mary, z/John\}$ .
Altre: $P(x,f(y))$ e $P(g(z),z)$ danno $\{z/f(y), x/g(f(y))\}$ ; $Q(x,x)$ e $Q(A,B)$ falliscono (costanti diverse); $Q(x,y)$ e $Q(y,A)$ danno $\{y/A, x/A\}$ ; $R(x,f(x))$ e $R(y,y)$ falliscono per occur check ( $y$ in $f(y)$ ).
CNF animali: $\forall x\ [\forall y\ Animal(y) \Rightarrow Loves(x,y)] \Rightarrow [\exists y\ Loves(y,x)]$ ; eliminare $\Rightarrow$ , $\neg$ dentro (con $\neg\forall \equiv \exists\neg$ ), standardizzare, Skolem ( $y \to F(x)$ , $z \to G(x)$ ), via $\forall$ , distribuire: $[Animal(F(x)) \lor Loves(G(x),x)] \land [\neg Loves(x,F(x)) \lor Loves(G(x),x)]$ . Controllato su dominio di $3$ oggetti, $4096$ interpretazioni, $0$ discordanze.
CNF cani: $\exists$ nell'antecedente diventa $\forall$ : $\neg Dog(y) \lor \neg Owns(x,y) \lor AnimalLover(x)$ (una clausola, niente Skolem).
CNF esami: $\forall x\ Student(x) \Rightarrow \exists y\ Exam(y) \land Passed(x,y)$ dà con $y \to F(x)$ le clausole $\neg Student(x) \lor Exam(F(x))$ e $\neg Student(x) \lor Passed(x,F(x))$ .
Errori tipici: dimenticare di standardizzare; Skolem con costante dentro un $\forall$ ; legare $v/t$ senza occur check; non applicare ai termini successivi i legami trovati.

Teoria collegata

Logica del primo ordine - unificazione, forward e backward chaining