Appunti completi corso Intelligenza Artificiale

B

Questo modello è molto usato per studiare il funzionamento di macchinari di ogni tipo (un

satellite, un’automobile…) oppure per fare la WHAT IF ANALYSIS, in cui studi cosa

succede dati certi input. Il processo di derivare nuova conoscenza dalla KB è chiamato

INFERENZA. La scrittura KB |= α significa che dalla KB, attraverso un algoritmo di

i

inferenza i, posso derivare α. Una procedura di inferenza banale potrebbe essere quella di

elencare tutte le lettere che trovi, e hai così che dalla KB ottieni tutte le formule A, B, C, D,

E, F. Ma non ha senso! Funziona sintatticamente, ma semanticamente no, perché non c’è

nulla nella KB che ti fa logicamente derivare E ed F. L’inferenza ha senso con

l’ENTAILMENT, ovvero che KB |= α ha senso se, ogni volta che KB è vero, anche A è

i

vero, cioè c’è conseguenza semantica. Nella logica proposizionale ciò si può fare in

modo molto semplice. Se hai un assegnamento alla KB che rende KB vero, allora

quell’assegnamento è detto MODELLO per KB. Se in una procedura di inferenza si ha che

ogni modello di KB è anche modello di α, allora la procedura è detta SOUND (corretta). La

nostra procedura di inferenza che elenca tutte le variabili non è sound, perché le variabili

che otteniamo non sono un conseguenza logica della KB. Poi se una procedura di

inferenza trova tutte le conseguenze logiche della KB, essa è detta COMPLETE. Se

dovessi scegliere una sola di queste due proprietà, ovviamente la migliore sarebbe la

soundness. La procedura di inferenza è una cosa legata alla sintassi, alla manipolazione

delle formule, per cui è un algoritmo. L’entailment invece è legato alla semantica.

Ragioniamo ora in termini di logica del prim’ordine. È ovviamente più potente. La logica

proposizionale è basata su fatti che sono o veri o falsi. Puoi dire se la temperatura è

superiore o inferiore ad un certo valore, ma non puoi dire che la temperatura vale, che so,

50 gradi. Nella logica del prim’ordine invece abbiamo oggetti, funzioni su questi oggetti e

relazioni tra gli oggetti. Questa è una descrizione dell’ambiente molto più ricca. Per

quanto riguarda la sintassi, gli oggetti sono rappresentabili con costanti o variabili. Poi

simboli funzionali per rappresentare le funzioni e simboli relazionali per rappresentare le

relazioni. Tra gli operatori logici si aggiungono i quantificatori. La semantica è data

dall’assegnamento ai predicati e alle variabili.

Naturalmente anche qui vale il discorso della conseguenza semantica, sulla soundness e

completeness. Una cosa molto interessante è che nei domini finiti delle variabili possiamo

“proposizionalizzare” delle formule del prim’ordine. In pratica, se hai un “per ogni” devi

esplicitamente ricopiare la formula per ogni assegnamento possibile (cosa che puoi fare

perché il dominio è finito). La KB proposizionale che ottieni è detta INFERENZIALMENTE

EQUIVALENTE. Naturalmente lo puoi fare anche con il quantificatore esistenziale usando

un trucchetto, che è la Skolemizzazione: togli il quantificatore ma sostituisci la variabile

quantificata con una costante. Però questa trasformazione in logica proposizionale NON

FUNZIONA se la KB ha delle funzioni, perché puoi sostituire i parametri delle funzioni con

altre funzioni e così ricorsivamente all’infinito, anche se il dominio è finito! Questo per il

fatto che la logica del prim’ordine è semi-decidibile in tante cose, ovvero se voglio provare

che una formula è vera, il processo può finire oppure durare all’infinito. Se una formula

non è conseguenza logica, il processo non finisce mai dicendoti “no” e ciò dipende da

questo fatto. Se una formula è effettivamente conseguenza logica, prima o poi ti dirà “sì”.

È per questo motivo che trasformiamo il prim’ordine in proposizionale quando possiamo,

perché questa logica è decidibile ed è anche analizzabile in modo molto efficiente.

Ora vediamo come derivare nuova conoscenza partendo da un insieme di formule, la KB.

Lo scopo è capire se una formula α è conseguenza semantica della KB. La prima

procedura che vediamo è chiamata FORWARD CHAINING: la KB però deve contenere

solo DEFINITE CLAUSES, cioè delle frasi che sono o delle singole lettere enunciative,

oppure una serie di lettere unite in AND che implicano una sola lettera enunciativa. Del

tipo A, B, C and D → E… Se questa condizione è verificata, allora il forward chaining può

usare questa regola di inferenza chiamata MODUS PONENS, ovvero se ho A e A → B

allora genero B. Nota quindi che con il modus ponens puoi derivare solo altre lettere

enunciative, cioè derivi dei fatti.

Dal punto di vista implementativo, le formule sono memorizzate non come stringhe ma

come alberi. In una KB con sole definite clause, il forward chaining è sound e complete.

Vuol dire che tutte le lettere generate sono vere, e che trova tutte le lettere enunciative che

sono vere. Inoltre questo algoritmo termina sempre in una condizione finale in cui ha

scoperto tutta la conoscenza che c’è.

Ora passiamo ad una procedura più complicata: la RISOLUZIONE. La KB stavolta può

essere generica, con qualsiasi tipo di frase. Però affinché possiamo applicare la

risoluzione, dobbiamo trasformare la KB in una forma chiamata CNF (CONJUNCTIVE

NORMAL FORM), che sarebbe la seconda forma canonica. Ogni frase è composta da

sottofrasi collegate in AND e le sottofrasi hanno delle lettere enunciative collegate in OR.

Le sottofrasi sono chiamate CLAUSOLE, e le clausole sono formate da una congiunzione

di letterali (i letterali sono un simbolo dritto o un simbolo negato). Se hai due clausole in

cui compare lo stesso letterale, e in una è dritto e nell’altra negato, si dice che le due

clausole sono COMPLEMENTARI.

Come trasformare un insieme di frasi in forma CNF? Con quattro fasi:

- Eliminazione delle doppie implicazioni: una formula del tipo A ↔ B è equivalente a (A →

B) and (B → A)

- Eliminazione delle implicazioni: una formula del tipo A → B è equivalente a not A or B

- Spostamento interno delle negazioni: significa spostare il not in modo che si trovi

esclusivamente davanti ad una singola lettera enunciativa. Qui è utile usare De Morgan,

oltre alla doppia negazione. Quindi not (A and B) = not A or not B mentre not (A or B) =

not A and not B

- Distribuzione degli or sugli and: qui bisogna riordinare le cose in modo da avere una CNF

Una volta ottenuto un insieme di clausole, ecco la regola di risoluzione: date due

clausole, se esse sono complementari (cioè un letterale compare dritto in una e negato

nella seconda), puoi generare una nuova clausola in cui quel letterale non compare più.

Come consideriamo le clausole? Beh in una KB tutte le frasi sono vere, quindi possiamo

vedere la KB come un gigantesco insieme di clausole unite in and. Se arrivi a generare la

clausola vuota, succede che la tua KB è INSODDISFACIBILE: non esiste un

assegnamento alle lettere affinché tutte le regole siano vere. Questa situazione viene

rivelata dalla risoluzione se trova la clausola vuota. Ciò è causato dal fatto che ottieni due

regole contenenti una A e l’altra not A e ovviamente non possono essere entrambe vere.

Data questa caratteristica, se ci chiedono se una frase α è derivabile dalla KB, basta

seguire questi passi:

- Traduci la KB in CNF

- Aggiungi alla CNF la clausola not α

- Prova a derivare la clausola vuota con la risoluzione

Se ottieni la clausola vuota allora α è conseguenza della KB. Percα deve essere negata?

Beh la dimostrazione formale è complicata, però io ho scoperto una dimostrazione

“grafica” che è geniale.

Vabbè fa vedere il metodo sistematico e poi quello con l’albero che è più intelligente. Poi

durante lo svolgimento a mano si possono applicare vari trucchi per velocizzare il tutto: per

esempio se hai una clausola del tipo A or not A or C la puoi trasformare in C. Oppure una

clausola con A or A la trasformi in A (si chiama FATTORIZZAZIONE). Anche qui la

risoluzione è sound e complete, e l’algoritmo raggiunge sempre un punto fisso MA devi

usare la fattorizzazione, se no potrebbe inutilmente continuare all’infinito.

Un altro metodo di inferenza si chiama MODEL CHECKING. Si cerca di dimostrare che

KB |= α controllando se ogni modello di KB è anche modello per α. Ma richiede un tempo

esponenziale… I model checking però usa un modo efficiente per controllare proprio

questo. L’algoritmo che vediamo si chiama DPLL, che brutto nome. Comunque è semplice

ed ha un approccio diverso dalle regole di inferenza viste prima. Si prende α, la si mette

negata dentro la KB, si ottiene una enorme CNF e si verifica se questa è insoddisfacibile.

Ci vuole quindi un algoritmo per verificare se una formula in CNF è soddisfacibile o meno:

è lo stesso usato per risolvere il SAT. Ma guarda caso si tratta di un CSP… devi

assegnare dei valori (vero o falso) a delle variabili (le lettere enunciative). Si parte dal

modello vuoto e si segue il classico algoritmo di assegnamento per i CSP. Però ci sono

metodi appositi per ottimizzare questo algoritmo visto che siamo nel mondo esponenziale,

come metodi intelligenti per la scelta delle variabili da assegnare e metodi per fermarsi in

largo anticipo.

Per esempio ci fermiamo quando è chiaro che non c’è una soluzione nel branch in cui ci

troviamo. Come ce ne accorgiamo? Se una singola clausola è falsa nel modello costruito

finora, possiamo già dire che dobbiamo tornare indietro. Perché? Perché le clausole sono

collegate in and, quindi devono essere tutte vere per prima cosa. Un CSP normale si

ferma quando non ha più assegnamenti possibili, qui invece ci fermiamo quando una

clausola è falsa, visto che possiamo sempre assegnare quello che vogliamo. Allo stesso

modo, se in una clausola assegniamo il valore vero ad un letterale dritto, sappiamo già

che quella clausola è vera e non la consideriamo più. Si chiama EARLY TERMINATION

HEURISTIC.

Poi c’è anche il trucco per scegliere una variabile. Metti caso che hai una clausola del tipo

B or C e B è falso, devi per forza assegnare vero a C. Si chiama SINGLE UNIT

HEURISTIC: se hai una singola variabile per rendere vera una clausola, la scegli e ci dai

l’assegnamento che rende il letterale vero. Se in una clausola un letterale è falso, puoi

toglierlo e potresti finire nella situa