Inferenza nella logica proposizionale in PL...A7 Inferenza in PL Paolo Salvaneschi 1 A7_3 V1.7...

A7 Inferenza in PL Paolo Salvaneschi 1

A7_3 V1.7

Inferenza nella logica proposizionale

Intelligenza Artificiale

Paolo Salvaneschi

Università di BergamoFacoltà di Ingegneria

Il contenuto del documento è liberamente utilizzabile dagli studenti, per studio personale e per supporto a lezioni universitarie.Ogni altro uso è riservato, e deve essere preventivamente autorizzato dall’ autore.

Sono graditi commenti o suggerimenti per il miglioramento del materialeNota: è utilizzato in parte il materiale didattico associato al testo di Stuart J. Russell, Peter Norvig

A7 Inferenza in PL Paolo Salvaneschi 2A7 Inferenza in PL Paolo Salvaneschi 2

INDICE

• Inferenza• Inferenza per enumerazione di modelli• Applicazione in sequenza di regole di inferenza• Risoluzione• KB in clausole di Horn• Forward chaining• Backward chaining• Confronto forward/backward


Inferenza

• Inferenza– Procedura che, applicata ad una base di conoscenza,

deriva una frase α implicata logicamente dalla base di conoscenza KB

KB α


Inferenza

• Concetti che si applicano a tutte le logiche– Equivalenza logica– Validità– Soddifacibilità

• Equivalenza logica• Due frasi sono logicamente equivalenti se e solo se sono

vere nello stesso insieme di modelli

α β β αiff eα β


Inferenza

• Equivalenze logiche


Inferenza

• Validità• Una frase è valida se è vera in tutti i modelli

(tautologia)• Es P ∨ ¬P è valida


Inferenza

• Soddisfacibilità• Una frase è soddisfacibile se è vera in almeno un

modelloα è vera nel modello mm soddisfa αm è un modello (esempio) di α

• Modo di verifica: enumerare tutti i possibili modelli fino a che se ne trova uno che soddisfa

• Problema NP-completo


Inferenza

• Relazione tra validità e implicazione logica (Relazione tra Implicazione logica e implicazione materiale)

• Deduction theorem

Per ogni formula α e β,α β

se e solo sela formula α⇒ β è valida

(sempre vera, in tutti i modelli)


A B A ⇒ B

Inferenza

• EsempioKB α

1111

1001

1010

1000

P Q P ∧Q P ∧ Q ⇒ Q

KB αα KB

KB implica logicamente αα è vero in tutti i modelliin cui KB è vero

KB ⇒ α è verain tutti i modelli

P ∧ Q Q


Inferenza

• Esempio

KB α

1111

1001

1010

1000

P Q P ∧Q P ∧ Q ⇒ Q

KB αα KB

Se KB ⇒ α non fosse vera in tutti i modelli allora ci sarebbe un caso in cui è falsa e quindi (tavola della verità della implicazione materiale)P ∧Q (KB) è vero e Q (α) è falso. α non è quindi vero in tutti i modelli in cui KB è vero e quindi non è implicato logicamente da KB

A B A ⇒ B


α βse e solo se

la formula α ∧ ¬ β è non soddisfacibile(mai vera, in nessun modello)

Inferenza

• Relazione tra soddisfacibilità e implicazione logica

• Prova per contraddizione o refutazione(reductio ad absurdum). Assumiamo β falsa. Ciò porta ad una contraddizione con α


Inferenza

• Inferenza– Procedura che, applicata ad una base di conoscenza,

deriva una frase α implicata logicamente dalla base di conoscenza KB

• Pattern di ragionamento in PL – Regole di inferenza– Prova: applicazione di una sequenza di regole di

inferenza (algoritmo di inferenza).

KB α


Inferenza per enumerazione di modelli

• Primo algoritmo di inferenza: inferenza per enumerazione (model checking)

– Implementazione diretta della definizione

Si enumerano i modelliSi verifica che in ogni modello in cui KB è vero α sia vero (tavola della verità)(un modello fissa il valore vero o falso di ogni simbolo proposizionale)

KB α


True

False

True

True

TrueTrueTrueTrue

FalseFalseFalseTrue

TrueFalseTrueFalse

FalseFalseFalseFalse

P Q P ⇒ Q (P ⇒ Q) ∧P Q

Modello di α (in cui α è vero)

Modello di KB (in cui KB è vero)

KB αSi verifica che in ogni modello in cui KB è vero α sia vero

Ogni riga è un possibile modello

Ogni colonna dice se la corrispondente

frase (simbolo proposizionale) èvera nei possibili

modelli



Insieme deimodelli di αM(α)

Insieme deimodelli di KBM(KB)

Si verifica che in ogni modello in cui KB è vero α sia vero

KB |= α se e solo se M ( KB ) ⊆ M (α )“Se KB è vero allora α deve essere vero”



True

False

True

True

TrueTrueTrueTrue

FalseFalseFalseTrue

TrueFalseTrueFalse

FalseFalseFalseFalse

P Q P ⇒ Q (P ⇒ Q) ∧P Q

Solo se: consideriamo un modello in cui α è falso.KB risulterà falso


KB α


Inferenza

• Alternativamente, per verificare che KB αpotremmo utilizzare il teorema di deduzionee verificare che

KB ⇒ α(P ⇒ Q) ∧P ⇒ Q

è valida (è sempre vera)



• Utilizzando l’inferenza per enumerazione abbiamo verificato che la base di conoscenza

α⇒ β α

β

KB = {α ⇒ β α}

Implica logicamente β

Regola di inferenza



• Algoritmo corretto (implementa direttamente la definizione di implicazione logica)

• e completo (esamina esaustivamente un numero finito di modelli)

• Complessità– Tempo: O(2n) per n simboli (in KB e α)

– Spazio: O(n) (depth first)• L’implicazione proposizionale è un problema co-

NP-completo co-NP complemento di NP: Per ogni problema di decisione in NP c’è un corrispondente problema in co-NP con le risposte si e noinvertiteco-NP- completo idem


Applicazione in sequenza di regole di inferenza

• Altri algoritmi di inferenza (alternativa a enumerazione di modelli): applicazione in sequenza di regole di inferenza (prova)– Trovare una prova è come trovare una soluzione ad un

problema di ricerca– Le regole di inferenza possono essere usate come

operatori su KB utilizzando i metodi di ricerca nello spazio degli stati

– Funzione successore:genera tutte le possibili applicazioni di regole di inferenza



• Regole di inferenza• Scritte nella seguente forma

A1…..An

A

Premesse

Conclusione


• Regole di inferenza• Equivalenze logiche (vedi sopra)• Modus ponens

• And-Elimination


α⇒ β α

β

α ∧ β

α

α ∧ β

β


• Esempio: procedura di inferenza iApplico due volte la regola “modus ponens”


α⇒ β α

β

Modus ponens

KB = {felino ⇒ animale, gatto ⇒ felino, gatto}

gatto ⇒ felino gatto

felino

felino ⇒ animale felino

animale

KB animalei

Passo 1

Passo 2

Conclusione



• Confronto tra :– inferenza per enumerazione (model checking)– applicazione in sequenza di regole di inferenza (prova,

dimostrazione)• NP-completa• Nel caso peggiore la prova non è più efficiente della enumerazione

dei modelli• In pratica può essere più efficiente poiché ignora proposizioni

irrilevanti (le proposizioni non considerate dalle inferenze applicate) mentre l’algoritmo che enumera gli stati della tavola di verità le considera tutte (vedi nota)


nota• I sistemi logici esaminati sono monotoni• Se si aggiunge informazione alla base di conoscenza,

l’effetto è che l’insieme delle frasi implicate logicamente può solo crescere

• Aggiungendo informazione ciò che è vero prima non diventa falso, semplicemente si aggiungono nuove verità

• Logiche non monotone


Se KB α allora KB ∧ β α


nota• I sistemi logici esaminati sono monotoni• Nell’esempio precedente si utilizza la regola di inferenza

Modus Ponens applicandola più volte a piccole porzioni di KB – Località

• Se la logica proposizionale non fosse monotona bisognerebbe considerare ogni volta l’intera KB e non sarebbe possibile modificarla incrementalmente



Risoluzione

• Le regole sono corrette (sound)• Gli algoritmi di inferenza che usano

l’applicazione in sequenza di regole di inferenza sono corretti (sound)

• Sono completi?• L’algoritmo di ricerca può essere completo, ma

l’algoritmo di inferenza può non essere completo se la scelta delle regole di inferenza non èadeguata


Risoluzione

• Risoluzione• Una sola regola di inferenza che, unita a un

algoritmo di ricerca completo, genera un algoritmo di inferenza completo

• La risoluzione è corretta e completa per PL


Risoluzione

• Clausole• Una clausola è una disgiunzione di letterali

Letterale: frase atomica (letterale positivo) o frase atomica negata (letterale negativo)

• Un letterale è considerato come una disgiunzione di un letterale (clausola unitaria)

• Letterali complementari: uno la negazione dell’altro


Risoluzione

• Esempio: Clausole di lunghezza due• La risoluzione prende due clausole e produce una

nuova clausola che contiene tutti i letterali delle due originali, eccetto i letterali complementari


• Unit resolution inference ruleletterale letterali complementari

• Full resolution inference ruleletterali complementari

eliminato

Risoluzione

eliminato

eliminato

eliminato


• La clausola risultante deve contenere solo una copia di ogni letterale (fattorizzazione)

A ∨ B A ∨ ¬ B

A ∨ A

A ∨ A

A

Risoluzione


Risoluzione

• La regola di risoluzione è applicabile solo a disgiunzioni di letterali

• Si dimostra che ogni frase nella logica delle proposizioni è logicamente equivalente a una congiunzione di disgiunzioni di letterali

• Forma normale congiuntiva (CNF – ConjunctiveNormal Form)

Es. (A ∨ ¬ B ) ∧ (B ∨ ¬ C ∨ ¬ D)


• L’algoritmo di risoluzione (per refutazione)– Nota: la risoluzione non può essere utilizzata per

enumerare le frasi vere (generare le conseguenze) ma solo per confermare o rifiutare una frase

• Una procedura di inferenza basata sulla risoluzione utilizza il seguente schema:Prova per contraddizione. Per dimostrare che

si dimostra che (KB ∧ ¬α) è non soddisfacibile

Risoluzione

KB α


– (KB ∧ ¬α) è convertito in CNF– La regola di risoluzione è applicata alle clausole

risultanti– Ogni coppia di clausole che contiene letterali

complementari è risolta ed è aggiunta all’insieme fino a che:

• Non è più possibile aggiungere nuove clausole:KB non implica α

• E’ derivata una clausola vuota (equivale a False – può avere origine solo dalla risoluzione di due clausole unitarie complementari es. P e ¬P) (contraddizione) :KB implica α

Risoluzione


Risoluzione

• Esempio di risoluzione

(KB ∧ ¬α) convertita in CNF

Risoluzione

clausola vuotaKB implica α

Tutte le clausole ottenute risolvendo le coppie della riga sopra


Risoluzione

Nota

B 1,1 ∨ ¬ B 1,1 ∨ P 1,2

True ∨ P 1,2

Trueeliminata


KB in clausole di Horn

• Clausole di Horn• Le basi di conoscenza reali possono contenere clausole

appartenenti ad una classe con una restrizione chiamate Clausole di Horn. Per esse esiste una procedura di inferenza in tempo polinomiale.

• Clausole di Horn:Disgiunzione di letterali di cui al massimo uno è positivo

(¬ A ∨ ¬ B ∨ C )

(¬ B ∨ C ∨ D)

è una clausola di Horn

Non è una clausola di Horn



• Utilizzo delle Clausole di Horn• Ogni clausola di Horn può essere scritta come una

implicazione la cui premessa è una congiunzione di letterali positivi e la cui conclusione è un unico letterale positivo

• Modo facile da leggere usato nelle basi di conoscenza

(A ∧ B ⇒ C )(Se lo spostamento K1 è intermedio

e lo spostamento K2 è elevatoallora lo stato è preallarme)

Regola


• Esempio


¬ A ∨ ¬ B ∨ C(¬ A ∨ ¬ B ) ∨ C associatività di ∨

¬(A ∧ B ) ∨ C De Morgan

A ∧ B ⇒ C eliminazione dell’implicazione



• Utilizzo delle Clausole di Horn• L’inferenza con le clausole di Horn può essere eseguita

applicando il Modus Ponens ovunque possibile, fino a quando non si può eseguire alcuna inferenza.

• L’inferenza con le clausole di Horn può essere eseguita con gli algoritmi forward chaining e backward chaining. Facili da capire

• Complessità per decidere l’implicazione logica: lineare rispetto alle dimensioni di KB



• Clausole di Horn: Disgiunzione di letterali di cui al massimo uno è positivo

• Definite clauses (base per la programmazione logica): Disgiunzione di letterali di cui esattamente uno è positivo

(¬ A ∨ ¬ B )E’ una Horn clauseNon è una definite Horn clause

(¬ A ∨ ¬ B ∨ C ) E’ una definite Horn clause

headbody

( C ) fact



Nota: Horn clause senza letterali positivi: cosa è?

(¬ A ∨ ¬ B ) E’ una Horn clauseNon è una definite Horn clause

¬(A ∧ B )

¬(A ∧ B ) ∨ False

(A ∧ B ) ⇒ False E’ un vincolo di integrità(database)

Voto <30 e lode ⇒ False



• Algoritmi di Forward-chaining e Backward-chaining

• Inferenza su una base di conoscenza costituita da una congiunzione di Clausole di Horn

• Complessità lineare rispetto alle dimensioni di KB• Es di KB:


Forward-chaining

• Forward-chaining• Schema:

– Problema: q (query) è implicata da KB ?– Inizia dai fatti conosciuti (letterali positivi) in KB– Se le premesse di una implicazione sono vere,

aggiunge la conclusione all’insieme dei fatti conosciuti in KB

– Procede fino a che è aggiunta q oppure non si può piùinferire nulla

• Sound e completa


Forward-chaining

Esempio

Grafo AND-ORequivalente

AND

ORbody head


Forward-chaining


Forward Chaining

Count: quante premesse di un’implicazione sono sconosciuteSe il contatore arriva a zero tutte le premesse sono note e la conclusione può essere aggiunta a KB

Simboli inizialmente noti come veri (in agenda)

Query


Forward Chaining


Forward Chaining

Simbolo inferito (in inferred)


Forward Chaining


Forward Chaining

Simbolo giàprocessato. Non èaggiunto a KBEvita ridondanze e loop


Forward Chaining


Forward Chaining

• Forward----Data Driven• Il processo di ragionamento è diretto dai dati che sono

propagati attraverso la base di conoscenza, deducendo nuovi fatti

• Nell’esempio il ragionamento ha lo scopo di rispondere ad una specifica query (q è vero?)

• Il ragionamento diretto dai dati può essere anche utilizzato senza una query

• L’agente riceve dei dati sensoriali e inferisce delle conclusioni. Es. interpretazione automatica di un insieme di dati di misura


Forward Chaining

• Forward----Data Driven• Durante il processo di ragionamento è possibile che, nel

grafo AND-OR, siano attivabili più regole contemporaneamente.

• Possono essere utili meccanismi esterni che decidono quale attivare tra le regole attivabili


Forward Chaining

L’algoritmo propaga i dati di ingressoe,quando trova STOP si ferma.Sia R1 che R2 sono attivabiliPuò aver senso attivare R2 (regola più specifica che contienepiù fatti in ingresso)

Misura A alta Misura B alta

Allarme--STOP

Allarmegrave --STOP

R1 R2

Dati di ingresso


Backward -chaining

• Backward-chaining• Schema

– Idea: procedere all’indietro dall’obiettivo q: per dimostrare q tramite KB, verifica se q è già dimostrato, or dimostra tramite KB tutte le premesse di una regola che ha q come conclusione

– Evitare i cicli: verificare che le premesse non siano già state nella lista dei simboli da verificare

– Evitare la duplicazione di lavoro: verifica se una premessa da verificare1) è già stata provata vera2) ha già portato al fallimento


Backward -chaining

Per dimostrare vero Q bisogna dimostrare vero P (sotto-obiettivo)Obiettivi

Q


Backward -chaining

Per dimostrare vero Pbisogna dimostrare veri M e LObiettivi

PQ


Backward -chaining

Obiettivi

LMPQ


Backward -chaining

Per dimostrare vero Mbisogna dimostrare veri B e LB è un fattoL è già da dimostrare vero

Per dimostrare vero LBisogna dimostrare vero (P and A) or (B and A)P è un sotto-obiettivo già considerato

Bisogna dimostrare vero B e AB e A sono fatti

ObiettiviABLMPQ


Backward -chaining

A B C

LOR

Quale si sceglietra il sotto-obiettivo A e la coppia di sotto-obiettivi B,C ?

Es. l’ultimo inserito nello stack. Se fallimento si ritorna indietro e si prova la coppia (il successivo insieme di sotto-obiettivi)

(Esplorazione depth first dell’albero AND / OR)

Nota


Backward -chaining

B e A è vero


Backward -chaining

L è vero se B e A sono veri

Obiettivi

LMPQ


Backward -chaining

Quindi L è vero


Backward -chaining

M è vero se L e B sono veri

Obiettivi

MPQ


Backward -chaining

Quindi M è vero


Backward -chaining


Backward -chaining

• Backward----Goal Driven• Adatta alla soluzione di problemi (verifica di ipotesi)• (il componente xx è guasto?, Il paziente ha l’epatite?)

• Complessità lineare rispetto alle dimensioni di KB• In realtà può essere molto meno di lineare:

il ragionamento considera solo i fatti rilevanti


Confronto Forward - Backward

• Forward----Data driven– Non ci sono definite ipotesi da testare– Il risultato del ragionamento dipende dalla situazione

corrente (il ragionamento inizia dai fatti disponibili)– Es.Problemi di configurazione, interpretazione dati

• Backward----Goal Driven– Esistono delle ipotesi definite da testare (il

ragionamento inizia dalle ipotesi)– Il numero delle ipotesi è limitato– Es. Problemi di diagnosi medica, di apparati

Inferenza nella logica proposizionale in PL...A7 Inferenza in PL Paolo Salvaneschi 1 A7_3 V1.7...

Documents

Transcript of Inferenza nella logica proposizionale in PL...A7 Inferenza in PL Paolo Salvaneschi 1 A7_3 V1.7...