Cap5 logica proposizionale

LOGICA PROPOSIZIONALE

Corso di Intelligenza ArtificialeA.A. 2009/2010

Prof. Ing. Fabio Roli

Corso di Intelligenza Artificiale A.A. 2009/2010 Logica proposizionale

Prof. Ing. F. Roli 2

Introduzione

La logica proposizionale (LP) prende in considerazione schemi proposizionali composti da

• simboli di proposizioni (variabili proposizionali)

• connettivi, cioè operatori che agiscono su intere proposizioni e producono proposizioni più complesse

In questo capitolo si descriveranno

• la sintassi della LP, cioè le regole che definiscono le sue formule ben

formate (quelle a cui è possibile attribuire un significato)

• la semantica della LP, cioè il significato delle sue formule

• i principali algoritmi di inferenza della LP



Connettivi estensionali

I principali connettivi considerati nella logica classica sono di tipo estensionale: il valore di verità delle proposizioni da essi prodotte dipende solo dai valori di verità delle proposizioni su cui agiscono

I principali connettivi estensionali sono i seguenti

• “non” (negazione), indicata con il simbolo !

• “o” (disgiunzione), indicata con il simbolo "

• “e” (congiunzione) , indicata con il simbolo #

• “se... allora...” (implicazione) , indicata con il simbolo $

Si dimostra che i connettivi #, !, oppure ", !% consentono di definire tutti gli altri possibili connettivi estensionali. Da questo punto di vista i quattro connettivi precedenti sono ridondanti, ma è comodo usarli tutti per ridurre la complessità delle formule



Connettivi non estensionali: esempio

La congiunzione “perché” è un connettivo: infatti se P e Q sono proposizioni, lo è anche “P perché Q”

Si considerino le tre proposizioni seguenti, tutte vere:

• P1: “I pesci non sopravvivono fuori dell’acqua”

• P2: “I pesci respirano con branchie”

• P3: “I pesci sono animali a sangue freddo”

È facile vedere che “P1 perché P2” è vera, mentre “P1 perché P3” è falsa. Quindi il valore di verità di una proposizione della forma “P perché Q” non dipende solo dai valori di verità di P e Q



Connettivi estensionali: osservazioni

Nel linguaggio naturale l’unico connettivo propriamente estensionale è “non”, mentre gli altri possono produrre enuciati che possono non essere considerati proposizioni, dei quali cioè non abbia senso chiedersi se siano veri o falsi. Esempi:

• “Il treno è arrivato in ritardo e tutti gli uomini sono mortali”

• “Se 5 è pari, allora Tokio è la capitale del Giappone”

Gli enunciati componenti non sono “pertinenti” tra loro

In alcuni casi il connettivo “se... allora...” è non estensionale. Es.:• P: “Se la terra fosse più lontana dal Sole, allora sarebbe più fredda”

• Q: “Se la terra fosse più lontana dal Sole, allora sarebbe più calda”

Le proposizioni componenti sono tutte false, ma mentre P è vera, Q è falsa

Quindi in realtà i connettivi “e”, “o” e “se... allora...” considerati nella logica sono un’astrazione dei corrispondenti connettivi del linguaggio naturale, dei quali si trascurano gli aspetti non estensionali



Sintassi della logica proposizionale

Indicando con lettere maiuscole (P, Q, R, ...) le variabili proposizionali, le formule ben formate (fbf) della LP sono definite ricorsivamente dalle regole seguenti

• le variabili P, Q, R, ... sono fbf (atomiche)

• se ! è una fbf qualsiasi, !! è una fbf (non atomica)

• se ! e " sono fbf qualsiasi, ! # ", ! " " e ! $ " sono fbf (non atomiche)

• nient’altro è una fbf

Si noti che l’ultima regola ha la funzione di escludere esplicitamente qualsiasi formula che non sia ottenuta secondo le tre regole precedenti

È utile includere tra le fbf atomiche anche i simboli True e False, i cui valori di verità sono sempre, per definizione, rispettivamente vero e falso



Precedenza dei connettivi e profondità di una fbf

L’ordine di precedenza dei connettivi (a partire da quello con precedenza maggiore) è per convenzione !% #% "% $

Per specificare un ordine diverso (oppure per rendere più semplice la comprensione di una formula) si usano le parentesi tonde

Esempio: !P " Q # R $ S è equivalente a !((P " (Q # R)) $ S)

Si dice sottoformula di una fbf non atomica ogni fbf in essa contenuta

Es.: (P # Q) "(R$S) contiene le sottoformule (P # Q) e (R$S), che a loro volta contengono le sottoformule (atomiche) P, Q, R e S

Si può quindi vedere una qualsiasi fbf non atomica come composta ricorsivamente da insiemi di sottoformule a diversa profondità

La fbf dell’esempio precedente è composta dalle sottoformule (P#Q) e &R$S) che hanno per definizione profondità 1, e a loro volta sono composte dalle fbf atomiche P, Q, R e S che hanno profondità 2



Formalismo di Backus-Naur (BNF)

La sintassi (o grammatica) di ogni linguaggio formale può essere definita in modo rigoroso per mezzo del formalismo di Backus-Naur

In tale formlismo le formule di un linguaggio sono definite come un insieme di stringhe costituite da una sequenza di simboli

I componenti di una grammatica nel formalismo BNF sono:• un insieme di simboli terminali, con i quali si costruiscono le formule• un insieme di simboli non terminali che identificano parti delle

formule• un simbolo iniziale che identifica una formula completa• un insieme di regole di riscrittura della forma LHS ' RHS, che

definiscono le fbf attraverso la definizione ricorsiva di simboli non terminali in funzione di altri simboli qualsiasi

– LHS è un simbolo non terminale– RHS è una sequenza di zero o più simboli qualsiasi



Esempio: sintassi BNF per espressioni aritmetiche

Si considerino espressioni aritmetiche composte da numeri interi e dalle quattro operazioni fondamentali, come per es. (4 + 5) ( 8

La sintassi delle espressioni di tale linguaggio è la seguente

• Expr ' Expr Operator Expr | ( Expr ) | Number

• Number ' Digit | Number Digit

• Digit ' 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9• Operator ' + | – | ÷ | (

Gli elementi di tale sintassi sono i seguenti

• Expr è il simbolo iniziale, e rappresenta una qualsiasi formula del linguaggio

• Number, Digit e Operator sono i simboli non terminali• Le dieci cifre decimali e i simboli +, ), ÷, ( sono i simboli terminali

Si noti che il simbolo | è usato per indicare più definizioni alternative della LHS di una regola di riscrittura



Esempio: sintassi BNF per espressioni aritmetiche

Le regole di riscrittura di una grammatica BNF possono essere usate per

• costruire fbf del linguaggio

• verificare se una data formula composta da simboli terminali è una fbf del linguaggio

Per es., seguendo le regole precedenti è facile verificare che “12”, “3+7”, e “(4 + 5) – (2 ( 8)” sono fbf, mentre non lo sono “4+”, “9 ÷ = 7”, “() 5”

NOTA: i simboli usati nella sintassi di un linguaggio non ne determinano la semantica. Nel linguaggio appena definito si sono usati simboli di uso comune in aritmetica, ai quali si associa un significato convenzionale ben noto. Tuttavia a tale linguaggio sarebbe possibile associare una semantica completamente diversa da quella usuale!



Sintassi BNF della logica proposizionale

Le regole che definiscono le fbf della LP possono essere ridefinite nel formalismo BNF nel modo seguente

Sentence ' AtomicSentence | ComplexSentence

AtomicSentence ' True | False | P | Q | R | ...ComplexSentence ' ( Sentence ) |

Sentence Connective Sentence |

! Sentence

Connective ' | | # " $



Semantica della logica proposizionale

La semantica di un linguaggio formale specifica il significato delle sue formule ben formate

Nel caso della LP con connettivi estensionali, la semantica definisce il valore di verità delle sue fbf, in funzione dei due elementi del linguaggio (variabili proposizionali e connettivi)

• variabili proposizionali: rappresentano proposizioni che possono essere vere oppure false

• connettivi: il valore di verità di una fbf composta ottenuta per mezzo di un connettivo estensionale dipende in modo funzionale dai valori di verità delle formule componenti (e dallo stesso connettivo). Ogni connettivo può cioè essere visto come una funzione di verità



Semantica dei connettivi

La semantica dei connettivi estensionali della LP può essere descritta per mezzo delle tavole di verità

La semantica dei quattro connettivi principali è definita come segue (P e Q indicano fbf qualsiasi, non necessariamente atomiche)

P !PFalse TrueFalse TrueTrue FalseTrue False

P Q P $ QFalse False TrueFalse True TrueTrue False FalseTrue True True

P Q P # QFalse False FalseFalse True FalseTrue False FalseTrue True True

P Q P " QFalse False FalseFalse True TrueTrue False TrueTrue True True



Semantica dei connettivi: osservazioni

Come anticipato in precedenza, la semantica dei connettivi della LP (a parte la negazione) è un’astrazione della semantica dei corrispondenti connettivi del linguaggio naturale

Dopo la definizione formale della loro semantica nella LP, sono opportune le seguenti ulteriori osservazioni

• il connettivo # è per definizione simmetrico (P#Q equivale a Q#P). Ma nel linguaggio naturale il connettivo “e” viene usato anche con altri significati. Per es., in “Si sposarono e ebbero un figlio”, “e” ha significato temporale, e quindi non è simmetrico (il significato di “Ebbero un figlio e si sposarono” è diverso)

• il connettivo “o” viene usato in LP con significato inclusivo (P"Q è vera se P o Q, oppure entrambe, sono vere), mentre in linguaggio naturale può avere significato esclusivo (“In una partita di tennis si può vincere o perdere”) (cont.)



Semantica dei connettivi: osservazioni

Per definizione, la formula P $ Q è falsa solo se P è vera e Q è falsa

Questa semantica è spesso in contrasto con quella del linguaggio naturale

Esempi• “Se 5 è dispari, allora Tokyo è la capitale del Giappone” è vera in LP

perché le due proposizioni componenti sono vere. Ma poiché tra i fatti che esse rappresentano non c’è rapporto di causa-effetto, in linguaggio naturale si tenderebbe a considerarla falsa. Tuttavia i connettivi estensionali considerano solo il valore di verità delle singole proposizioni componenti, non i rapporti tra i fatti rappresentati

• Se P è falsa, in LP P $ Q è vera indipendentemente dal valore di verità di Q (es.: “Se 5 è pari, allora Parigi è la capitale del Giappone”)

• Se P e Q sono false, in LP P $ Q è vera. Questo rispecchia casi come “Se la Terra fosse più lontana dal Sole, sarebbe più fredda”, ma non “Se la Terra fosse più lontana dal Sole, sarebbe più calda”



Determinazione del valore di verità di formule composte

Ogni assegnazione di valori di verità ai simboli proposizionali di una fbf è detta interpretazione. Una formula con n simboli ha 2n interpretazioni

Il valore di verità di una qualsiasi fbf composta può essere calcolato ricorsivamente in funzione di quello delle sue variabili proposizionali

• si costruisce una tavola di verità con una riga per ogni intepretazione delle variabili proposizionali della fbf

• si determina il valore di verità di ciascuna sottoformula composta, a partire da quelle a profondità maggiore, “risalendo” passo passo fino alla fbf originaria, per mezzo delle tavola di verità dei connettivi

Si noti che la tavola di verità di una fbf in cui compaiano n variabili proposizionali sarà composta da 2n righe



Valore di verità di formule composte: esempio

Si consideri la fbf ((P#Q) " (R$(!P))) che contiene 3 variabili proposizionali e ha profondità 2

Il suo valore di verità si può determinare per mezzo della tavola seguente, in cui per ogni sottoformula composta

• il valore di verità è indicato sotto il corrispondente connettivo

• la profondità è indicata sotto l’ultima riga

variabili proposizionali sottoformule

P Q R ((P#Q) " (R $( ! P)))

F F F F T T TF F T F T T TF T F F T T TF T T F T T TT F F F T T FT F T F F F FT T F T T T FT T T T T F F

1 0 1 2



Il connettivo di equivalenza

Per comodità è utile introdurre un nuovo connettivo, detto “equivalenza” e indicato con *, definito dalla tavola seguente (in parole, P*Q è vera se e solo se P e Q hanno lo stesso valore di verità)

È facile verificare che P*Q può essere riscritta come (P$Q)#(Q$P)

P Q P * QFalse False TrueFalse True FalseTrue False FalseTrue True True



Validità e soddisfacibilità

Sono due concetti legati alle relazioni di conseguenza e contraddizione, e quindi agli algoritmi di inferenza

• Una formula è valida (o tautologica) se è vera per tutte le possibili interpretazioniEs.: è evidente che True, !False, e (P " !P) sono valide (P denota in questo esempio una fbf qualsiasi)

• Una formula è soddisfacibile se è vera per almeno una (ma non tutte) le interpretazioni. Es.: P, P"Q (P e Q denotano in questo caso proposizioni atomiche, non fbf qualsiasi)

È facile vedere che, se una fbf qualsiasi P è valida, !P è contraddittoria



Un algoritmo di inferenza per la logica proposizionale

È ora possibile definire un algoritmo di inferenza che consenta di verificare se una data formula A (conclusione) è conseguenza di un dato insieme ! di formule (premesse)

L’algoritmo si basa sulla definizione di conseguenza e sulle tavole di verità dei connettivi:

• costruire una tavola di verità che comprenda tutte le 2n interpretazioni delle n variabili proposizionali che compaiono nelle premesse e nella conclusione

• verificare che A sia vera in tutte le interpretazioni in cui siano vere tutte le premesse

Si dimostra che tale algoritmo, detto model-checking, è corretto e completo. In particolare si osservi che, per ogni ! e A, l’algoritmo termina sempre in un numero finito di passi



Algoritmo model-checking: esempio

Dato l’insieme di fbf ! = {P"Q, P$R, Q$R}, verificare se le fbf P"R e Q#R siano conseguenza logica di !

La tavola di verità delle premesse è la seguente

variabili proposizionali premesse

P Q R P"Q P$R Q$R

F F F F T TF F T F T TF T F T T FF T T T T TT F F T F TT F T T T TT T F T F FT T T T T T





La tavola di verità delle premesse è la seguente

Le righe in cui tutte le premesse sono vere sono evidenziate in grigio

variabili proposizionali premesse

P Q R P"Q P$R Q$R

F F F F T TF F T F T TF T F T T FF T T T T TT F F T F TT F T T T TT T F T F FT T T T T T





La tavola di verità delle cinque fbf è la seguente

Le righe in cui tutte le premesse sono vere sono evidenziate in grigio

Come si vede, in tutti questi casi P"R è vera, mentre Q#R può essere falsa. Quindi P"R è conseguenza di !, mentre Q#R non lo è

variabili proposizionali premesse conclusioni

P Q R P"Q P$R Q$R P"R Q#R

F F F F T T F FF F T F T T T FF T F T T F F FF T T T T T T TT F F T F T T FT F T T T T T FT T F T F F T FT T T T T T T T



Esempio: il gioco del Wumpus

Come esempio di applicazione dei concetti visti finora, si consideri il gioco del Wumpus. Si consideri per semplicità la codifica della sola conoscenza riguardante i pozzi. Una possibile codifica fa uso delle seguenti variabili proposizionali

• Pi,j: “c’è un pozzo nella casella (i,j)”

• Bi,j: “c’è una corrente d’aria nella casella (i,j)”

NOTA: è necessaria una diversa variabile proposizionale per ogni casella... (le conseguenze verranno discusse più avanti)

Le regole del gioco riguardanti i pozzi (per semplicità, solo in alcune caselle) possono allora essere codificate dalle seguenti formule

R1: !P1,1

R2: B1,1 * (P1,2 " P2,1)

R3: B2,1 * (P1,1 " P2,2 " P3,1)



Esempio: il gioco del Wumpus

Si assuma che la configurazione della caverna sia quella indicata in figura, e che l’agente si sposti dalla casella di partenza alla (2,1)La conoscenza corrispondente alle percezioni nelle due caselle (e riguardante solo i pozzi) è allora codificata dalle formule

R4: !B1,1

R5: B2,1In definitiva, la base di conoscenza (KB) dell’agente dopo la prima mossa conterrà (tra le altre) le seguenti formule

R1: !P1,1

R2: B1,1 * (P1,2 " P2,1) R3: B2,1 * (P1,1 " P2,2 " P3,1)R4: !B1,1

R5: B2,1



Esempio di inferenza nel gioco del Wumpus

Si supponga ora che l’agente sia interessato alla presenza di pozzi nelle caselle (1,2) e (2,2), cioè, per es., al valore di verità delle fbf !P1,2 e P2,2

Dovrebbe allora verificare se tali fbf sono conseguenza delle formule presenti nella sua KB. Tale verifica può essere eseguita con l’algoritmo model-checkingConsiderando per semplicità il sottoinsieme di fbf della KB ! = {R1, ..., R5}, contenenti 7 simboli proposizionali, ciò comporta la costruzione di una tavola di verità con 27 = 128 righeDalla figura è facile verificare che {R1, ..., R5} sono tutte vere solo nei tre casi corrispondenti alla presenza di un pozzo in (2,2) o in (3,1) o in entrambe, e all’assenza di pozzi in (1,1), (1,2) e (2,1), e che in tali casi+!P1,2 è sempre vera

• P2,2 è invece vera solo nel caso in cui in (2,2) non ci sia un pozzo

Quindi ! |= !P1,2, ! |, P2,2. Allora l’agente può concludere che nella casella (1,2) non c’è un pozzo, ma non che ce ne sia uno in (2,2)



Limiti dell’algoritmo model-checking

L’algoritmo model-checking è completo nel senso che può dire se una qualsiasi fbf data sia o no implicata da un dato insieme di fbf !, ma non può essere usato per derivare automaticamente le fbf implicate da un dato insieme !Inoltre, se le premesse ! e la conclusione A contengono n simboli di proposizione, la tavola di verità corrispondente contiene 2n righe: l’algoritmo model-checking è quindi estremamente inefficiente, dato che la sua complessità è O(2n) (l’algoritmo è NP-completo)Questi limiti rendono necessarie

• la definizione di algoritmi di inferenza che consentano di derivare le fbf implicate da una data !

• la definizione di algoritmi di inferenza più efficienti del model-checking per la verifica della relazione !|=A (per una data A)

Entrambi gli obbiettivi richiedono la definizione di regole d’inferenza



Regole di inferenza

Le tavole di verità dei connettivi consentono di definire alcune regole di

inferenza, cioè regole che, da un insieme di formule (premesse) vere, consentono di ricavare una formula che segua da esse (conclusione)

Le regole di inferenza si rappresentano con la notazione

Di seguito si riportano alcune delle principali regole di inferenza della LP. La loro correttezza può facilmente essere verificata attraverso le tavole di verità, controllando che le conclusioni siano vere ogni volta che le premesse sono vere (si noti che le variabili che compaiono in ciascuna regola denotano fbf qualsiasi, non necessariamente atomiche)

premesse

conclusione



Regole di inferenza

! $ ", !

" (Modus ponens)

!1,!2 ,...,!n

!1 # !2 # ... # !n

(Introduzione di # )

!!!

! (Eliminazione della doppia negazione)

! * "

! $ "& -# " $ !& - (Eliminazione dell'equivalenza)

! ! # "& -

!! " !" (Prima legge di De Morgan)

! ! " "& -

!! # !" (Seconda legge di De Morgan)

! $ "

!" $ !! (Contrapposizione)



Regole di inferenza

Dato un insieme di premesse !, le regole d’inferenza (come quelle appena viste) possono essere usate per due scopi

• per derivare fbf logicamente implicate da !

• per verificare se una data fbf A segua da !

Informalmente, ciò avviene attraverso un’opportuna sequenza di passi che consistono nell’applicazione di regole di inferenza in cui si usino come premesse sia le fbf contenute in ! che quelle già derivate nei passi precedenti. Tale sequenza di passi è detta dimostrazione

Di seguito si mostrerà un esempio informale di dimostrazione per mezzo di regole d’inferenza, nel caso del gioco del Wumpus



Regole di inferenza: esempio

Si consideri la stessa configurazione della caverna mostrata nell’esempio precedente (riportata in figura), e le formule ! = {R1, ..., R5} che faranno parte della KB dell’agente dopo il suo primo spostamento nella casella (2,1)

R1: !P1,1

R2: B1,1 * (P1,2 " P2,1)

R3: B2,1 * (P1,1 " P2,2 " P3,1)

R4: !B1,1

R5: B2,1




In precedenza si è ottenuto con l’algoritmo model-checking ! |= !P1,2

Vediamo ora come !P1,2 possa essere derivata attraverso una sequenza di applicazioni di regole di inferenzaR1: !P1,1

R2: B1,1 * (P1,2 " P2,1)

R3: B2,1 * (P1,1 " P2,2 " P3,1)

R4: !B1,1

R5: B2,1

R6: (B1,1 $ (P1,2 " P2,1)) # ((P1,2 " P2,1) $ B1,1) R2, elimin. dell’equivalenzaR7: (P1,2 " P2,1) $ B1,1 R6, eliminazione di #

R8: !B1,1 $ !(P1,2 " P2,1) R7, contrapposizione

R9: !(P1,2 " P2,1) R8 e R4, modus ponens

R10: !P1,2 # !P2,1 R9, II legge di De Morgan

R11: !P1,2 R10, eliminazione di #




In precedenza si è ottenuto con l’algoritmo model-checking ! |= !P1,2

Vediamo ora come !P1,2 possa essere derivata attraverso una sequenza di applicazioni di regole di inferenzaLe formule derivate ad ogni passo verranno indicate con R6, R7, ..., e potranno essere usate come premesse nelle applicazioni di regole d’inferenza nei passi successivi. Per ogni passo si indica la regola usata e le formule usate come premesse

R6: (B1,1 $ (P1,2 " P2,1)) # ((P1,2 " P2,1) $ B1,1) R2, elimin. dell’equivalenzaR7: (P1,2 " P2,1) $ B1,1 R6, eliminazione di #

R8: !B1,1 $ !(P1,2 " P2,1) R7, contrapposizione

R9: !(P1,2 " P2,1) R8 e R4, modus ponens

R10: !P1,2 # !P2,1 R9, II legge di De Morgan

R11: !P1,2 R10, eliminazione di #



Un algoritmo basato su regole di inferenza

Formalmente, l’algoritmo basato su regole d’inferenza per derivare formule implicate da un dato insieme di premesse ! è il seguente

• applicare tutte le possibili regole d’inferenza a tutte le possibili premesse ottenibili da formule di !, e aggiungere a ! tutte le formule derivate che non si trovino già in !

• ripetere il passo precedente finché sia possibile derivare formule che non facciano già parte di !

Si noti che i possibili insiemi di formule composti da un dato insieme di premesse e da fbf implicate sono rappresentabili come uno spazio degli stati:

• ogni stato corrisponde a un possibile insieme !

• lo stato iniziale corrisponde all’insieme delle premesse

• la funzione “successore” applica in ogni modo possibile tutte le regole d’inferenza alle formule ! di uno stato. Ogni singola formula derivata A genera un nuovo stato ! . {A}

(cont.)




Ricavare le formule implicate corrisponde allora a costruire l’intero grafo degli stati a partire dallo stato iniziale (le premesse)

Problemi:

• lo spazio degli stati è finito?

• anche se lo spazio degli stati fosse finito, esiste un insieme di regole di inferenza che consente di ottenere un algoritmo completo? (cioè, che consenta di costruire l’intero spazio degli stati)

• ammesso che lo spazio degli stati sia finito, qual è la complessità computazionale di un tale algoritmo?




Se invece si volesse realizzare un algoritmo basato su regole d’inferenza per verificare se una data conclusione A è conseguenza di un dato insieme di premesse, si potrebbe formulare il problema come un problema di ricerca nello spazio degli stati definito in precedenza. Ogni stato il cui insieme di formule contiene A è uno stato obbiettivo

Problemi:

• il branching factor può essere molto elevato

• quale euristica si può usare per scegliere ad ogni passo il nodo da espandere? (si noti che nell’esempio di dimostrazione dato in precedenza, la formula !P1,2 è stata derivata in sei passi, scegliendo però ad ogni passo in modo accorto, rispetto all’obbiettivo, la regola di inferenza e le premesse corrispondenti)

• esiste un insieme di regole di inferenza che consenta di ottenere un algoritmo completo? (cioè che garantisca di trovare una dimostrazione di A, se ne esiste almeno una)



Algoritmi basati su regole di inferenza

Si vedrà ora come, attraverso l’uso di regole di inferenza, sia possibile definire algoritmi completi e più efficienti, e in particolare

• un algoritmo di inferenza completo basato sul modus ponens, che consente sia di derivare tutte le fbf che seguono da un dato insieme di premesse, sia di verificare se una data conclusione è conseguenza di un dato insieme di premesse, limitatamente a un sottoinsieme di fbf

della LP (dette clausole di Horn)

• un algoritmo di inferenza completo per l’intera LP (algoritmo di risoluzione), che consente di verificare se una data conclusione è conseguenza di un dato insieme di premesse

La maggiore efficienza di tali algoritmi è in parte dovuta al fatto che sono basati su una sola regola di inferenza



Clausole di Horn

In molti problemi di interesse pratico è possibile esprimere tutte le formule in forma di clausole di Horn, cioè implicazioni della forma

P1 # ... # Pn $ Q

in cui

• l’antecedente è una congiunzione di simboli proposizionali non negati

• il conseguente è un singolo simbolo proposizionale non negato

Attraverso l’equivalenza (P $ Q) * (!P " Q) (che vale sia per qualsiasi fbf P e Q, e può essere facilente verificata per mezzo delle tavole di verità), si ha che anche ogni simbolo proposizionale affermato o negato (detto letterale), può essere espresso in forma di clausola di Horn, sfruttando le seguenti equivalenze:

• P * (!True " P) * (True $ P)+!P * (!P " False) * (P $ False)



L’algoritmo forward chaining

Usando il modus ponens (MP) come unica regola d’inferenza, è possibile realizzare un algoritmo che derivi tutte le formule atomiche non negate implicate da un insieme di premesse ! in forma di clausole di Horn:

• si applica MP in ogni modo possibile alle formule di !• se non è possibile derivare formule che non facciano già parte di !,

l’algoritmo termina• si aggiungono a ! tutte le nuove formule derivate (si noti che tali

formule possono essere solo simboli proposizionali non negati), e si ripetono i passi precedenti

Si dimostra che questo algoritmo di inferenza, detto forward chaining

• è completo per simboli proposizionali non negati e premesse in forma di clausole di Horn

• ha complessità lineare rispetto alla dimensione della KB



L’algoritmo backward chaining

Il MP consente anche di realizzare un algoritmo completo per verificare se una qualsiasi formula atomica e non negata A sia implicata da un insieme di premesse ! in forma di clausole di Horn

• Date ! e A:– se A fa parte di !, allora si può concludere che KB |= !: la verifica ha

successo e l’algoritmo termina– si consideri il sottoinsieme !’ di clausole di ! che abbiano A come

conseguente; per ogni clausola di !’ si verifichi ricorsivamente se ogni proposizione nell’antecedente è implicata da !

– se la verifica ha successo per almeno una clausola di !’, allora si può concludere che !|=A, altrimenti si può concludere che !|,A

La formula da dimostrare è anche detta query (interrogazione)L’algoritmo è detto backward-chaining, poiché consiste nell’applicare “a ritroso” la regola MPLa sua complessità è inferiore rispetto al forward chaining



Forward chaining e backward chaining: osservazioni

L’algoritmo forward chaining non ha lo scopo di dimostrare una data formula, ma di derivare tutte le conseguenze di un dato insieme di formule: in questo senso è un algoritmo di inferenza di tipo data-driven

In un’applicazione come il gioco del Wumpus può essere utile per derivare dopo ogni azione dell’agente tutte le conseguenze delle nuove percezioni e della conoscenza già acquisita (si riveda l’esempio di ragionamento informale del capitolo precedente)Si noti che può anche essere usato per dimostrare una data formula A (basta verificare se al termine A si trovi tra le fbf derivate), ma non è efficiente per questo scopo (da questo punto di vista è analogo ad un algoritmo di ricerca non informata)

L’algoritmo backward chaining ha invece lo scopo di dimostrare una data formula, e in questo senso è una forma di ragionamento goal-directed, più efficiente del forward chaining



L’algoritmo di risoluzione

Si presenterà ora l’algoritmo di risoluzione, un algoritmo di inferenza completo per la LP nel senso che è in grado di verificare se una qualsiasi fbf data sia conseguenza di un qualsiasi insieme di premesse. Tale algoritmo è basato su

• la riscrittura di ogni fbf in forma normale congiuntiva

• una nuova regola di inferenza, detta di risoluzione



Conversione di formule in forma normale congiuntiva

Una fbf m1"..."mk formata dalla disgiunzione di letterali (simboli proposizionali affermati o negati) è detta clausola

Si dimostra facilmente che qualsiasi fbf della LP può essere riscritta in forma di congiunzione di clausole (forma normale congiuntiva, CNF) attraverso i passi seguenti (nel seguito, p, q e r indicano letterali):

• eliminazione delle implicazioni: (p $ q) * (!p " q)

• spostamento di ! verso l’interno, attraverso le leggi di De Morgan e l’eliminazione della doppia negazione:

!(p " q) * (!p # !q), !(p # q) * (!p " !q), !!p * p

• distribuzione degli # sugli ": ((p # q) " r) * ((p " r) # (q " r))

Esempio: B1,1 * (P1,2 " P2,1) diventa

(!B1,1 " P1,2 " P2,1) # (B1,1 " !P1,2) # (B1,1 " !P2,1)



La regola di inferenza di risoluzione

Si considerino due clausole !: p1"..."pm e ": q1"..."qn, tali che per qualche i e j pi e qj siano letterali complementari (uno è la negazione dell’altro, come P e !P)

La regola di risoluzione è la seguente:

La correttezza della regola si verifica facilmente: se pi è falso, allora qj è vero, e viceversa. Quindi o la disgiunzione degli m–1 letterali (escluso pi) di !, o la disgiunzione degli n–1 letterali (escluso qj) di ", o entrambe, sono vere. Ma allora è vera anche la disgiunzione dei m+n–2 letterali di ! e ", esclusi pi e qj

La conclusione della regola di risoluzione è detta risolvente

Come caso particolare, la risoluzione di due letterali complementari porta alla cosiddetta clausola vuota, indicata con []




L’algoritmo di risoluzione consiste nel costruire una dimostrazione per

refutazione (o per assurdo) di una data fbf A, a partire da un dato insieme di premesse !

Si ricordi che la dimostrazione per assurdo si basa sul fatto che ! |= A se e solo se ! . {!A} è contraddittorio

L’algoritmo richiede prima di tutto la riscrittura in CNF di !A e delle formule in !, e la separazione di tutti i congiunti

• es.: (!P " Q " R) # (Q " !R) # (R " !S) viene separata nelle tre formule distinte (!P " Q " R), (Q " !R) e (R " !S)

L’algoritmo consiste nella ripetizione del seguente passo a partire dall’insieme iniziale " = ! . {!A}:

• applicare la regola di risoluzione in ogni modo possibile alle formule di ", e inserire in " le formule derivate (se non ne fanno già parte)




Si dimostra che, dopo un numero finito di passi• se ! . {!A} è contraddittorio (cioè se ! |= A), dopo un numero finito di

passi si troverà in " almeno una coppia di letterali complementari (per es. P e !P)

• se invece ! . {!A} non è contraddittorio (cioè se ! |, A), allora dopo un numero finito di passi non sarà più possibile ottenere nuove formule, e non ci sarà in " nessuna coppia di letterali complementari

Le condizioni precedenti costituiscono dunque le condizioni di terminazione dell’algoritmo di risoluzione. Dopo ogni applicazione della regola di risoluzione:

• se " contiene almeno una coppia di letterali complementari, allora si può concludere che ! |= A, e l’algoritmo termina

• se " non contiene coppie di letterali complementari, e non è più possibile ottenere nuove formule, allora si può concludere che ! |, A, e l’algoritmo termina




Si noti che se un insieme di fbf contiene due letterali complementari, la sua contraddittorietà è evidente (e viene subito rilevata dall’algoritmo di risoluzione, senza eseguire nessun passo d’inferenza)

Esistono però anche insiemi contraddittori che non contengono coppie di letterali complementari (si vedano gli esempi del cap. precedente), la cui contraddittorietà non è quindi evidente

L’importanza dell’algoritmo di risoluzione consiste nel far emergere in modo esplicito la contraddittorietà di un insieme di fbf, attraverso la derivazione della forma più semplice di contraddizione, cioè una coppia di letterali complementari



Algoritmo di risoluzione: esempio

Si consideri il seguente insieme di fbf, chiaramente contraddittorio (poiché contiene tutte le combinazioni di tre variabili in clausole di tre disgiunti, in ciascuna delle quali ogni variabile compare una volta sola: quindi ognuna delle 23=8 clausole è falsa per una delle 23=8 possibili interpretazioni):P"Q"R, !P"Q"R, P"!Q"R, P"Q"!R, !P"!Q"R, !P"Q"!R, P"!Q"!R,!P"!Q"!R

Nella pagina seguente si mostra l’applicazione dell’algoritmo di risoluzione a tale insieme

• ogni clausola sarà scritta in una riga distinta e numerata• si scriveranno prima le otto clausole dell’insieme iniziale• poi si scriveranno le clausole ottenute come risolventi di coppie di clausole

precedenti (delle quali saranno indicati i numeri di riga)

Si noti che ad ogni passo possono esistere più coppie di clausole da risolvere: è quindi necessaria una scelta che può influenzare il numero di passi dell’algoritmo




1 P"Q"R2 !P"Q"R3 P"!Q"R4 P"Q"!R5 !P"!Q"R6 !P"Q"!R7 P"!Q"!R8 !P"!Q"!R9 Q"R 1,2

10 !Q"R 3,511 Q"!R 4,612 !Q"!R 7,813 R 9,1014 !R 11,1215 [] 13,14




Si consideri ora un insieme di clausole non contraddittorio, ottenuto per es. eliminando una qualsiasi clausola (diciamo !P " !Q " !R) da quello dell’esempio precedenteL’applicazione dell’algoritmo di risoluzione è mostrata a lato

Si osservi che l’algoritmo si arresta al passo 12 poiché non è più possibile ottenere nuove fbf applicando la regola di risoluzione alle fbf 1-12L’assenza di letterali complementari nelle fbf 1-12 indica che l’insieme di partenza 1-7 non è contraddittorio

1 P"Q"R2 !P"Q"R3 P"!Q"R4 P"Q"!R5 !P"!Q"R6 !P"Q"!R7 P"!Q"!R8 Q"R 1,29 !Q"R 3,5

10 Q"!R 4,611 R 8,912 Q 10,11




Si consideri ancora l’esempio del gioco del WumpusQuando l’agente si trova nella casella (1,1) (vedi figura) percepisce l’assenza di correnti d’aria: la sua KB conterrà tra le altre le formuleB1,1 * (P1,2 " P2,1) e !B1,1

Con un semplice ragionamento informale si può concludere che le due formule precedenti implicano !P1,2




Per dimostrarlo attraverso la regola di risoluzione, si effettuano prima i seguenti passi preliminari

• si trasforma B1,1 * (P1,2 " P2,1) in CNF, ottenendo le tre clausole(!B1,1 " P1,2 " P2,1), (B1,1 " !P1,2) e (B1,1 " !P2,1)

• si aggiunge la negazione della query !P1,2, cioè P1,2, alle premesse, ottenendo l’insieme di clausole{(!B1,1 " P1,2 " P2,1), (B1,1 " !P1,2), (B1,1 " !P2,1), !B1,1, P1,2}

Una possibile applicazione dell’algoritmo di risoluzione a tale insieme è mostrata a lato

1 !B1,1 " P1,2 " P2,1

2 B1,1 " !P1,2

3 B1,1 " !P2,1

4 !B1,1

5 P1,2

6 !B1,1 " B1,1 " P1,2 1,37 P1,2 " P2,1 " !P1,2 1,38 !B1,1 " B1,1 " P2,1 1,29 P1,2 " P2,1 " !P2,1 1,2

10 !P2,1 3,411 !P1,2 2,412 [] 5,11



Un agente per il mondo del Wumpusbasato sulla logica proposizionale

Negli esempi visti finora si è considerata la rappresentazione e l’elaborazione della conoscenza sulle caratteristiche “statiche” dell’ambiente (pozzi senza fondo e percezioni)

Si accennerà ora a come sia possibile rappresentare ed elaborare la conoscenza dell’agente con lo scopo di

• determinare l’azione da eseguire ad ogni passo• tener traccia della propria posizione• aggiornare la propria conoscenza in base alle percezioni ricevute dopo

l’esecuzione di ogni azione



Un agente per il mondo del Wumpusbasato sulla logica proposizionale

La strategia per determinare l’azione da eseguire ad ogni passo potrebbe essere espressa da formule come la seguente:

W1,2 # L2,2 $ !Left

dove Li,j e Wi,j indicano la posizione dell’agente e del Wumpus, mentre Left indica che l’azione da eseguire è uno spostamento verso sinistraPer decidere l’azione da eseguire ad ogni passo, l’agente potrebbe interrogare la KB con le query corrispondenti alle quattro azioni possibili, eseguendo una delle azioni corrispondenti alle query che risultassero verePer es., per sapere se, dato lo stato di conoscenza attuale sull’ambiente, la strategia codificata nella KB iniziale consiglia di spostarsi verso sinistra, l’agente deve verificare se la formula Left sia implicata dalla KB attualeQuesto potrebbe essere ottenuto in due modi

• con l’algoritmo di risoluzione per refutazione• se la KB è espressa in forma di clausole di Horn, si può usare l’algoritmo

backward chaining



Un agente per il mondo del Wumpusbasato sulla logica proposizionale (cont.)

Per tener traccia della posizione dell’agente si può pensare di usare formule come la seguente:

L1,1 # Right $ L2,1

Si noti che tali formule (come quelle che codificano la strategia dell’agente) fanno parte della conoscenza “a priori” (background knowledge) sull’ambiente, e devono perciò essere inserite nella KB iniziale dell’agente

Se la KB fosse espressa in forma di clausole di Horn, per aggiornarla in base alle percezioni ricevute dopo l’esecuzione di ogni azione:

• si inseriscono le formule corrispondenti alle percezioni nella KB (per esempio, !B1,1)

• si esegue l’algoritmo forward chaining



Un agente per il mondo del Wumpusbasato sulla logica proposizionale (cont.)

Il programma dell’agente può essere schematizzato come segue

function KB-AGENT(percept) returns an actionstatic: KB, a knowledge baset, a counter, initially 0, indicating timeTELL(KB, MAKE-PERCEPT-SENTENCE(percept,t))action / ASK(KB, MAKE-ACTION-QUERY(t))TELL(KB, MAKE-ACTION-SENTENCE(action,t))t / t + 1return action

• TELL(KB, !) inserisce la formula ! nella KB• ASK (KB, !) interroga la KB per dimostrare la formula !

Si noti che il meccanismo di inferenza è “nascosto” nelle due funzioni precedentiPer es., se la KB è espressa in forma di clausole di Horn:

• TELL può attivare l’algoritmo forward chaining per determinare tutte le conseguenze della formula inserita

• ASK può dimostrare la query con l’algoritmo backward chaining



Limiti della logica proposizionale

In teoria è possibile progettare un agente per il mondo del Wumpus basato sulla LP. Tuttavia, è facile accorgersi che questo comporta seri problemi dal punto di vista pratico. Per esempio:

• per rappresentare la posizione dell’agente è necessario un simbolo proposizionale diverso per ogni casella

• per rappresentare il fatto che nelle caselle adiacenti un pozzo c’è una corrente d’aria, è necessaria una formula diversa per ogni casella

• per descrivere la posizione dell’agente dopo uno spostamento, servirebbero quattro formule per ogni casella

– in realtà ne servono di più: infatti se l’agente si trova in (1,1), la KB contiene L1,1; se l’agente si sposta a destra, dopo L1,1 # Right $ L2,1 la KB conterrebbe anche L2,1!

– bisogna allora usare proposizioni come Lti,j, dove l’apice indica l’istante

di tempo, e regole come L11,1 # Right $ L2

2,1…

È evidente che il numero di simboli proposizionali e di formule necessarie per descrivere nel linguaggio della LP anche un problema semplice come quello del Wumpus è troppo elevato



Limiti della logica proposizionale

L’esempio precedente suggerisce che la capacità espressiva della LP sia troppo limitata per problemi reali

Nel capitolo seguente si descriverà la logica dei predicati, caratterizzata da una capacità espressiva molto maggiore della LP, e adatta alla descrizione di molti problemi reali

Cap5 logica proposizionale

Documents

Transcript of Cap5 logica proposizionale