Logica del primo ordine - unificazione, forward e backward chaining

Argomento del corso da 9 CFU. Fonte: slide del corso di Intelligenza Artificiale, Ing. dell'Informazione UniPD. Presuppone 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 → (CNF, risoluzione, conseguenza logica).

Dalla logica proposizionale al primo ordine

La logica proposizionale assume che il mondo contenga solo fatti. La logica del primo ordine (FOL, first-order logic) assume, come il linguaggio naturale, che contenga:

• oggetti: persone, case, numeri, teorie, colori, guerre, secoli;
• relazioni o proprietà: fratello di, più grande di, dentro, possiede, sta tra; rosso, rotondo, primo;
• funzioni (restituiscono un valore preciso): padre di, migliore amico di, uno in più di.

Elementi della sintassi:

• Termine: una costante, una variabile oppure $Funzione(Termine_1, \dots, Termine_n)$. Indica un oggetto.
• Enunciato atomico: $Predicato(Termine_1, \dots, Termine_n)$. Esprime un fatto che può essere vero o falso: $Brother(KingJohn, RichardTheLionheart)$.
• Enunciato complesso: enunciati atomici combinati con i connettivi, per esempio $Sibling(KingJohn, Richard) \Leftrightarrow Sibling(Richard, KingJohn)$.

Quantificatori

$\forall x\ P$ è vero se $P$ è vero per ogni oggetto $x$: è circa la congiunzione di tutte le istanze. $\exists x\ P$ è vero se $P$ è vero per almeno un oggetto: è circa la disgiunzione delle istanze.

Errore tipico con $\forall$. Il connettivo principale con $\forall$ è di norma $\Rightarrow$. "Tutti a Oxford sono intelligenti" è $\forall x\ At(x, Oxford) \Rightarrow Smart(x)$. Con $\land$, $\forall x\ At(x, Oxford) \land Smart(x)$ significa "tutti sono a Oxford e tutti sono intelligenti".

Errore tipico con $\exists$. Il connettivo principale con $\exists$ è di norma $\land$. "Qualcuno non a Oxford è intelligente" è $\exists x\ \neg At(x, Oxford) \land Smart(x)$. Con $\Rightarrow$, $\exists x\ \neg At(x, Oxford) \Rightarrow Smart(x)$ è vero anche se esiste una persona a Oxford (antecedente falso, implicazione vera a vuoto) o intelligente: dice molto meno.

Proprietà.

• $\forall x \forall y$ equivale a $\forall y \forall x$ (si scrive $\forall x,y$); lo stesso per $\exists$.
• $\exists x \forall y$ non equivale a $\forall y \exists x$: $\exists x \forall y\ Loves(x,y)$ è "c'è una persona che ama tutti", $\forall y \exists x\ Loves(x,y)$ è "ognuno è amato da qualcuno".
• Dualità: $\forall x\ Likes(x, IceCream) \equiv \neg \exists x\ \neg Likes(x, IceCream)$; $\exists x\ Likes(x, Broccoli) \equiv \neg \forall x\ \neg Likes(x, Broccoli)$.

Esempi di frasi per una KB:

• fratelli e sorelle sono fratelli: $\forall x,y\ Brother(x,y) \Rightarrow Sibling(x,y)$;
• "Sibling" è simmetrica: $\forall x,y\ Sibling(x,y) \Leftrightarrow Sibling(y,x)$;
• la madre è il genitore femmina: $\forall x,y\ Mother(x,y) \Leftrightarrow Parent(x,y) \land Female(x)$;
• un cugino di primo grado è figlio di un fratello di un genitore: $\forall x,y\ FirstCousin(x,y) \Leftrightarrow \exists p,s\ Parent(p,x) \land Parent(s,y) \land Sibling(s,p)$.

Sostituzioni

Un agente del Wumpus con una KB in FOL percepisce puzza, brezza e luccichio al tempo $t=5$: Tell(KB, Percept([Stench, Breeze, Glitter], 5)). Poi chiede Ask(KB, ∃a Action(a, 5)): la KB implica qualche azione? Sì, per esempio con la sostituzione $\{a/Grab\}$.

Definizione (sostituzione). Una sostituzione $\theta = \{v_1/t_1, \dots, v_n/t_n\}$ assegna un termine a ciascuna variabile. Dato un enunciato $S$, $S\theta$ è il risultato di applicare $\theta$ a $S$.

Esempio. $S = Smarter(x,y)$ e $\theta = \{x/Hillary, y/Bill\}$ danno $S\theta = Smarter(Hillary, Bill)$. Ask(KB, S) restituisce alcune o tutte le $\theta$ tali che $KB \models S\theta$.

Proposizionalizzazione

Con le sostituzioni si può ricondurre l'inferenza FOL a quella proposizionale.

Istanziazione universale (UI). Da $\forall x\ \alpha$ si ricava $\alpha$ con $x$ sostituita da un termine chiuso $g$ (senza variabili): $\forall x\ King(x) \land Greedy(x) \Rightarrow Evil(x)$ dà $King(John) \land Greedy(John) \Rightarrow Evil(John)$, ma anche $King(Father(John)) \land \dots$ e così via. Si può applicare più volte: la nuova KB è equivalente alla vecchia.

Istanziazione esistenziale (EI). Da $\exists x\ \alpha$ si ricava $\alpha$ con $x$ sostituita da una costante di Skolem $k$ che non compare altrove nella KB: $\exists x\ Crown(x) \land OnHead(x, John)$ dà $Crown(C_1) \land OnHead(C_1, John)$, con $C_1$ nome inventato. Si applica una volta per eliminare l'enunciato esistenziale; la nuova KB non è equivalente alla vecchia, ma è soddisfacibile se e solo se lo era la vecchia.

Se l'esistenziale sta dentro un $\forall$, la costante diventa una funzione di Skolem delle variabili universali: $\forall x\ \exists y\ Soulmate(y,x)$ dà $\forall x\ Soulmate(F(x), x)$, che è diverso da $\forall x\ Soulmate(C_2, x)$ (la seconda dice che c'è un'unica anima gemella per tutti).

Esempio. KB: $\forall x\ King(x) \land Greedy(x) \Rightarrow Evil(x)$, $King(John)$, $Greedy(John)$, con soli tre oggetti $John, Richard, Henry$. Istanziando la prima regola in tutti i modi si ottengono $3$ enunciati ($King(John) \land Greedy(John) \Rightarrow Evil(John)$ e gli analoghi per Richard e Henry) più i $2$ fatti: i simboli proposizionali sono $King(John)$, $Greedy(John)$, $Evil(John)$, $King(Richard)$, ecc. Si risolve come nella logica proposizionale.

Problemi.

• Genera moltissimi enunciati irrilevanti: con $\forall y\ Greedy(y)$ si producono $Greedy(Richard)$, $Greedy(Henry)$ anche solo per provare $Evil(John)$.
• Con i simboli di funzione gli oggetti diventano infiniti: $Father(John)$, $Father(Father(John))$, $Father(Father(Father(John)))$, ...

La soluzione è cercare direttamente la sostituzione che serve: l'unificazione.

Unificazione

Nell'esempio, per ricavare $Evil(John)$ basta trovare $\theta$ che faccia combaciare $King(x)$ e $Greedy(x)$ con $King(John)$ e $Greedy(y)$: $\theta = \{x/John, y/John\}$.

Definizione (unificazione). $Unify(\alpha, \beta) = \theta$ con $\mathrm{Subst}(\theta, \alpha) = \mathrm{Subst}(\theta, \beta)$. Se non esiste $\theta$ l'unificazione fallisce.

L'ultimo fallimento è fittizio: le due $x$ appartengono a enunciati diversi, ma hanno lo stesso nome. Si risolve standardizzando (standardize apart) cioè rinominando le variabili di uno dei due: con $Knows(z, Mary)$ si ha $\{x/Mary,\ z/John\}$. Nei calcoli si rinominano sempre le variabili di una clausola prima di unificarla con un'altra.

Come si procede, regola per regola, confrontando i due termini da sinistra a destra:

1. due termini identici: si prosegue senza legare nulla;
2. una variabile e un termine $t$: si lega $v/t$, solo se $v$ non compare in $t$ (occur check);
3. due termini composti: servono lo stesso simbolo di funzione o predicato e lo stesso numero di argomenti, e poi si unificano gli argomenti a coppie, applicando le sostituzioni già trovate;
4. in ogni altro caso (due costanti diverse, costante contro composto, simboli diversi) si fallisce.

Occur check. $x$ e $Father(x)$ non si unificano: $x = Father(x)$ richiederebbe un termine infinito $Father(Father(Father(\dots)))$. Senza il controllo l'algoritmo non terminerebbe o sarebbe scorretto. Prolog di solito non lo fa (vedi Prolog - fatti, regole, ricorsione, liste e cutProlog come logica del primo ordine ristretta alle clausole di Horn: fatti, regole, query, motore di inferenza (backward chaining in profondità con backtracking, ordine delle clausole), termini, unificazione e occur check, aritmetica con is, ricorsione, liste e operatore barra, length e append, cut verde e rosso, cut e fail, negazione come fallimento.Prolog - fatti, regole, ricorsione, liste e cut →).

Il $\theta$ restituito è il più generale (most general unifier): ogni altro unificatore se ne ottiene con un'ulteriore sostituzione. Per esempio $Knows(John, x)$ e $Knows(y, z)$ danno $\{y/John, x/z\}$, non $\{y/John, x/Jane, z/Jane\}$.

# variabili: stringhe minuscole; costanti: stringhe maiuscole; composti: tuple ("F", arg1, ...)
def is_var(t): return isinstance(t, str) and t[0].islower()

def walk(t, s):                       # segue i legami già fatti
    while is_var(t) and t in s: t = s[t]
    return t

def occurs(v, t, s):                  # v compare dentro t?
    t = walk(t, s)
    return t == v or (isinstance(t, tuple) and any(occurs(v, a, s) for a in t[1:]))

def unify(a, b, s=None):              # restituisce la sostituzione, o None se fallisce
    s = {} if s is None else s
    a, b = walk(a, s), walk(b, s)
    if a == b: return s
    if is_var(a) or is_var(b):
        v, t = (a, b) if is_var(a) else (b, a)
        return None if occurs(v, t, s) else {**s, v: t}   # occur check
    if isinstance(a, tuple) and isinstance(b, tuple) and a[0] == b[0] and len(a) == len(b):
        for x, y in zip(a[1:], b[1:]):
            s = unify(x, y, s)
            if s is None: return None
        return s
    return None

def subst(t, s):                      # applica la sostituzione fino in fondo
    t = walk(t, s)
    return (t[0],) + tuple(subst(a, s) for a in t[1:]) if isinstance(t, tuple) else t

a, b = ("Knows", "John", "x"), ("Knows", "y", ("Mother", "y"))
s = unify(a, b)
print({v: subst(t, s) for v, t in s.items()})                  # {'y': 'John', 'x': ('Mother', 'John')}
print(unify(("Knows", "John", "x"), ("Knows", "x", "Mary")))   # None
print(unify("x", ("Father", "x")))                             # None (occur check)

Gli esempi di unificazione svolti sono in Esercizio - Unificazione e conversione in CNF nel primo ordine (slide del corso).

Risoluzione nel primo ordine

Come nel caso proposizionale: si converte $KB \land \neg\alpha$ in CNF e si applica la risoluzione; se si ottiene la clausola vuota, $KB \models \alpha$ (dimostrazione per assurdo).

Regola di risoluzione in FOL. Date due clausole standardizzate (con variabili diverse), con $\theta = Unify(l_i, \neg m_j)$: $$\frac{l_1 \lor \dots \lor l_i \lor \dots \lor l_k \qquad m_1 \lor \dots \lor m_j \lor \dots \lor m_n}{\mathrm{Subst}\big(\theta,\ l_1 \lor \dots \lor l_{i-1} \lor l_{i+1} \lor \dots \lor l_k \lor m_1 \lor \dots \lor m_{j-1} \lor m_{j+1} \lor \dots \lor m_n\big)}$$

Esempio. Da $\neg Rich(x) \lor Unhappy(x)$ e $Rich(Ken)$, con $Unify(\neg Rich(x), \neg Rich(Ken)) = \{x/Ken\}$ si ottiene $Unhappy(Ken)$.

Il sistema è completo per refutazione: se la KB implica $\alpha$, la clausola vuota si deriva. Ma il problema è solo semidecidibile: se $\alpha$ non è implicata, l'algoritmo può non terminare mai.

Conversione in CNF

I passi sono quelli proposizionali, più la gestione di variabili e quantificatori. Esempio: "chi ama tutti gli animali è amato da qualcuno", $$\forall x\ [\forall y\ Animal(y) \Rightarrow Loves(x,y)] \Rightarrow [\exists y\ Loves(y,x)].$$

1. Eliminare $\Leftrightarrow$ e $\Rightarrow$: $\forall x\ \neg[\forall y\ (\neg Animal(y) \lor Loves(x,y))] \lor [\exists y\ Loves(y,x)]$.
2. Portare $\neg$ all'interno, ricordando $\neg\forall x\ p \equiv \exists x\ \neg p$ e $\neg\exists x\ p \equiv \forall x\ \neg p$: $\forall x\ [\exists y\ \neg(\neg Animal(y) \lor Loves(x,y))] \lor [\exists y\ Loves(y,x)]$, poi con De Morgan e doppia negazione $\forall x\ [\exists y\ Animal(y) \land \neg Loves(x,y)] \lor [\exists y\ Loves(y,x)]$. Le due $y$ sono variabili diverse, che per caso hanno lo stesso nome.
3. Standardizzare le variabili (un nome diverso per ogni quantificatore): $\forall x\ [\exists y\ Animal(y) \land \neg Loves(x,y)] \lor [\exists z\ Loves(z,x)]$.
4. Skolemizzare: ogni $\exists$ è dentro $\forall x$, quindi diventa una funzione 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)$.
5. Togliere i $\forall$ (restano impliciti): $[Animal(F(x)) \land \neg Loves(x,F(x))] \lor Loves(G(x),x)$.
6. Distribuire $\lor$ su $\land$: $$[Animal(F(x)) \lor Loves(G(x),x)] \land [\neg Loves(x,F(x)) \lor Loves(G(x),x)].$$

Due clausole. (Verifica: su tutte le $4096$ interpretazioni di $Animal$ e $Loves$ su un dominio di $3$ oggetti, l'enunciato originale è vero se e solo se esistono due funzioni $F, G$ che rendono vera la CNF: è la proprietà che la Skolemizzazione garantisce.)

Esempio: Colonnello West

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. Dimostrare che West è un criminale.

Enunciati in logica, con le convenzioni che i nemici dell'America sono ostili e i missili sono armi:

1. $American(x) \land Weapon(y) \land Sells(x,y,z) \land Hostile(z) \Rightarrow Criminal(x)$
2. $Enemy(Nono, America)$
3. $Enemy(x, America) \Rightarrow Hostile(x)$
4. $\exists x\ Owns(Nono, x) \land Missile(x)$: con EI, $Owns(Nono, M_1) \land Missile(M_1)$ ($M_1$ costante di Skolem)
5. $Missile(x) \Rightarrow Weapon(x)$
6. $Missile(x) \land Owns(Nono, x) \Rightarrow Sells(West, x, Nono)$
7. $American(West)$

Dimostrazione per risoluzione di $KB \models Criminal(West)$. Clausole della KB (variabili già distinte per ogni clausola):

• $K_1$: $\neg American(x) \lor \neg Weapon(y) \lor \neg Sells(x,y,z) \lor \neg Hostile(z) \lor Criminal(x)$
• $K_2$: $American(West)$
• $K_3$: $\neg Missile(x) \lor Weapon(x)$
• $K_4$: $Missile(M_1)$
• $K_5$: $\neg Missile(x) \lor \neg Owns(Nono,x) \lor Sells(West,x,Nono)$
• $K_6$: $Owns(Nono, M_1)$
• $K_7$: $\neg Enemy(x, America) \lor Hostile(x)$
• $K_8$: $Enemy(Nono, America)$
• $K_9$: $\neg Criminal(West)$ (negazione della tesi)

Clausola vuota: $KB \land \neg Criminal(West)$ è insoddisfacibile, quindi $Criminal(West)$ sì. (I passi sono stati rieseguiti con un piccolo programma Python che applica l'unificazione a ogni passo.) La versione svolta come esercizio è Esercizio - Risoluzione, forward e backward chaining sul caso Criminal West (slide del corso).

Clausole definite, forward e backward chaining

La risoluzione completa può essere lenta. Se la KB ha solo clausole definite (definite clauses: disgiunzione con esattamente un letterale positivo, cioè implicazioni $p_1 \land \dots \land p_n \Rightarrow q$ e fatti) si usano due algoritmi più semplici. Il caso dell'esempio vale: tutti gli enunciati 1-7 sono definiti. I fatti ($Owns$, $Missile$, $Enemy$, $American$) sono clausole definite con corpo vuoto.

Backward chaining (concatenazione all'indietro)

Parte dalla domanda e la verifica ricorsivamente all'indietro: per dimostrare un obiettivo si cerca una clausola la cui conseguenza si unifica con esso, e si dimostrano le premesse con la sostituzione propagata. È una ricerca in profondità (vedi Ricerca nello spazio degli stati - formulazione dei problemi e ricerca non informataUn agente risolutore di problemi è un agente basato su obiettivi con rappresentazione atomica: formula un problema (stato iniziale, azioni, modello di transizione, test dell'obiettivo, costo dei passi) e cerca una sequenza di azioni che porta a uno stato obiettivo costruendo un albero di ricerca. Le strategie non informate usano solo la definizione del problema e si distinguono per l'ordine di espansione della frontiera: ampiezza (coda FIFO), costo uniforme (coda con priorità sul costo g), profondità (pila LIFO), profondità limitata, approfondimento iterativo e ricerca bidirezionale. Si confrontano per completezza, ottimalità, tempo e spazio in funzione di b, d, m; tutte sono casi di best-first search con una diversa funzione di valutazione f.Ricerca nello spazio degli stati - formulazione dei problemi e ricerca non informata →): non ottima ma molto efficiente. Si applica solo a KB di fatti e implicazioni. È ciò che fa Prolog.

Traccia su $Criminal(West)$ (ogni riga: obiettivo, clausola usata, sostituzioni nuove; le variabili delle clausole sono rinominate a ogni uso):

Criminal(West)            <- regola 1, {x/West}
  American(West)          <- fatto, {}
  Weapon(y)               <- regola 5, {y/x'}
    Missile(x')           <- fatto Missile(M1), {x'/M1}      quindi y = M1
  Sells(West, M1, z)      <- regola 6, {z/Nono, x''/M1}
    Missile(M1)           <- fatto, {}
    Owns(Nono, M1)        <- fatto, {}
  Hostile(Nono)           <- regola 3, {x'''/Nono}
    Enemy(Nono, America)  <- fatto, {}

Tutte le foglie sono fatti: $Criminal(West)$ è dimostrato con $\{x/West, y/M_1, z/Nono\}$. Un solo ramo di ricerca, nessun tentativo inutile: nella risoluzione servono tutti i passi sopra e in più si potrebbero generare clausole irrilevanti.

Forward chaining (concatenazione in avanti)

Parte dai fatti e applica ripetutamente le regole le cui premesse sono già tutte note, aggiungendo le conseguenze, finché non si ricava la domanda o non c'è più nulla di nuovo (punto fisso). Su questa KB:

• Giro 1 (fatti: $American(West)$, $Missile(M_1)$, $Owns(Nono,M_1)$, $Enemy(Nono,America)$): $Missile(x) \Rightarrow Weapon(x)$ con $\{x/M_1\}$ dà $Weapon(M_1)$; $Missile(x) \land Owns(Nono,x) \Rightarrow Sells(West,x,Nono)$ con $\{x/M_1\}$ dà $Sells(West,M_1,Nono)$; $Enemy(x,America) \Rightarrow Hostile(x)$ con $\{x/Nono\}$ dà $Hostile(Nono)$.
• Giro 2: la regola 1 ha ora tutte le premesse, con $\{x/West, y/M_1, z/Nono\}$: nasce $Criminal(West)$.
• Giro 3: nessuna conseguenza nuova, punto fisso.

(Giri e fatti controllati con un programma Python.) Il forward chaining è corretto e, per clausole definite senza simboli di funzione, termina sempre; ricava però tutte le conseguenze, anche le irrilevanti per la domanda. Il backward chaining è invece guidato dall'obiettivo.

Ingegneria della conoscenza

L'ingegneria della conoscenza (knowledge engineering) è il processo di costruzione di una KB. I passi:

1. identificare le domande (analogo al PEAS dell'agente);
2. raccogliere la conoscenza rilevante;
3. scegliere un vocabolario di predicati, funzioni e costanti (ontologia);
4. codificare la conoscenza generale del dominio;
5. codificare la descrizione dell'istanza di problema;
6. porre domande al motore di inferenza e leggere le risposte;
7. correggere e valutare la KB.

Esempio: circuito sommatore. Domande: il circuito somma correttamente? Se tutti gli ingressi sono alti, qual è l'uscita della porta $A_2$? Quali porte sono collegate al primo terminale di ingresso? Ci sono anelli di retroazione? Conoscenza: i circuiti sono fatti di fili e porte; i segnali vanno lungo i fili ai terminali di ingresso delle porte; ogni porta produce un segnale sul terminale di uscita; i tipi di porta sono AND, OR, XOR (due ingressi) e NOT (uno).

Vocabolario: ogni porta è un oggetto con nome costante, per esempio $Gate(X_1)$, $Circuit(C_1)$, $Terminal(T_1)$; il tipo con una funzione, $Type(X_1) = XOR$. Regola generale: $\forall t_1,t_2\ Terminal(t_1) \land Terminal(t_2) \land Connected(t_1,t_2) \Rightarrow Signal(t_1) = Signal(t_2)$. Istanza: $Connected(Out(1,X_1), In(1,X_2))$ ("l'uscita $1$ di $X_1$ è collegata all'ingresso $1$ di $X_2$"). Domanda: per quali ingressi di $C_1$ l'uscita di $A_1$ vale $0$?, cioè $\exists i_1,i_2,i_3\ Signal(In(1,C_1)) = i_1 \land Signal(In(2,C_1)) = i_2 \land Signal(In(3,C_1)) = i_3 \land Signal(Out(1,A_1)) = 0$. Per il debug si perturba la KB togliendo o modificando regole e fatti per vedere quali comportamenti errati compaiono.

Domande d'esame

1. Unificare $Knows(John, x)$ e $Knows(x, Mary)$. Fallisce se si lasciano le due $x$ con lo stesso nome (si dovrebbe avere $x = John$ e $x = Mary$). Dopo aver standardizzato la seconda come $Knows(y, Mary)$ si ottiene $\{y/John, x/Mary\}$.
2. Tradurre "chi possiede un cane ama gli animali" e dare la CNF. $\forall x\ (\exists y\ Dog(y) \land Owns(x,y)) \Rightarrow AnimalLover(x)$. Eliminando l'implicazione e portando $\neg$ dentro, l'$\exists$ dell'antecedente diventa $\forall$: $\forall x,y\ \neg Dog(y) \lor \neg Owns(x,y) \lor AnimalLover(x)$. Una sola clausola, senza Skolem.
3. Skolemizzare $\forall y\ \exists x\ Loves(x,y)$ e $\exists x\ \forall y\ Loves(x,y)$. Il primo dà $Loves(F(y), y)$ (funzione di $y$, perché l'amante dipende da chi è amato); il secondo $\forall y\ Loves(C, y)$ con costante $C$.
4. Perché l'occur check? Senza, $x$ si unificherebbe con $Father(x)$ in un termine infinito, e l'algoritmo non terminerebbe o dedurrebbe cose sbagliate. Con il controllo l'unificazione di $x$ con $Father(x)$ fallisce.