Prof. Francesco Trovò

Corso di Intelligenza Artificiale, a.a. 2017-2018

Agenti Basati su Logica

09/04/2018

Agenti basati sulla logica

• Generico agente logico

• Il mondo del Wumpus

• Logica proposizionale

• Inferenza negli agenti logici

Agenti basati sulla conoscenza

Idea: il ragionamento umano non si basa semplicemente su

comportamenti reattivi, ma su modelli ben precisi del mondo

Da questa intuizione possiamo derivare degli agenti basati sulla

conoscenza, ovvero che operano ragionamenti su una

rappresentazione interna del mondo

Va oltre alla ricerca: nelle situazioni di incertezza non fa altro che

elencare tutti i possibili stati (stati credenza)

Va oltre ai CSP: passo verso una rappresentazione più completa degli

stati

Utilizzo della logica: possono adattarsi ai cambiamenti dell’ambiente e

può integrare nuova conoscenza nel modello

Proprietà dell’ambiente

• Completamente osservabile / parzialmente osservabile

• Agente singolo / multiagente

• Deterministico / stocastico

• Episodico / sequenziale

• Statico / dinamico / semidinamico

• Discreto / continuo

• Noto / ignoto

La base della conoscenza

L’insieme di tutte le formule che compongono le basi su cui si fondano i

ragionamenti dell’agente viene chiamata Knowledge Base (KB)

Ogni formula della KB è un assioma: non deve essere dimostrata, ma è

presa per buona dall’agente

Il processo di inferenza del programma agente aggiunge delle formule

alla KB esistente tramite due funzioni:

• Tell: comunica all’agente le percezioni avute

• Ask: restituisce l’azione da eseguire data la percezione corrente

• Tell: l’azione eseguita viene registrata nella base delle conoscenza

Caratteristiche degli Agenti Basati sulla

Conoscenza

Determino il comportamento dell’agente rispetto a ciò che conosce e al

suo obbiettivo (livello della conoscenza), che è indipendente dal

funzionamento dell’agente (livello dell’implementazione)

Differente approccio per la specifica del comportamento dell’agente:

• Approccio dichiarativo: passo all’agente la conoscenza necessaria

per raggiungere l’obbiettivo

• Approccio procedurale: codifico direttamente i comportamenti voluti

in un programma

Un agente efficace deve riuscire ad integrare entrambi gli approcci

Il mondo del Wumpus

Voglio trovare l’oro ed uscire

Se cado in un pozzo o finisco

nella casella del Wumpus

muoio

Posso tirare una sola freccia

Percezione:

[fetore, brezza, luccichio, urto, ululato]

Esempio di inferenza

Percezione:

[nulla, nulla, nulla, nulla, nulla]

Percezione:

[nulla, brezza, nulla, nulla, nulla]

Esempio di inferenza

Percezione:

[fetore, nulla, nulla, nulla, nulla]

Percezione:

[fetore, brezza, scintillio, nulla, nulla]Tutti i miei ragionamenti sono

corretti se è corretta la percezione!

Formule logiche

Le basi della conoscenza sono formate da formule logiche che hanno:

• Sintassi: definisce se sono ben formate

• Semantica: definisce se sono vere rispetto ad un mondo possibile

Una formula 𝛼 soddisfa il modello 𝑚 (ovvero la scelta delle variabili da

assegnare) se è vera 𝛼 in un modello 𝑚.

I modelli in cui 𝛼 è vera si dicono modelli di 𝛼 e sono denotati da 𝑀(𝛼)

Conseguenza logica

Una formula logica 𝛼 consegue logicamente da un’altra formula logica 𝛽se e solo se 𝑀 𝛼 ⊆ 𝑀 𝛽 , ovvero 𝛼 è un’affermazione più forte di 𝛽

𝛼1: “Non c’è un pozzo in [1,2]” 𝛼2: “Non c’è un pozzo in [2,2]”

Model checking

Model checking: enumero tutti i possibili modelli per verificare se 𝛼 è

vera in ogni modello ( 𝑀 𝐾𝐵 ⊆ 𝑀 𝛼 )

Vorrei trovare le formule 𝛼 che sono soddisfatte in KB

Per fare ciò ho la necessità di sviluppare delle procedure di inferenza

Dico che 𝛼 è derivato da 𝐾𝐵 attraverso la regola 𝑖 o 𝐾𝐵 ⊢𝑖 𝛼 se

l’algoritomo di inferenza è in grado di ricavare 𝛼 da 𝐾𝐵

Un algoritmo di inferenza è corretto se preserva la verità delle formule

ovvero se deriva formule che sono conseguenze logiche della base di

conoscenza

Un algoritmo di inferenza è completo se può derivare ogni formula che

è conseguenza logica della base di conoscenza

Logica proposizionale: sintassi

Formule atomiche: composte da un solo simbolo proposizionale ovvero

ogni simbolo rappresenta una proposizione che può essere vera o falsa

Formule complesse: composte da formule atomiche e da connettivi

logici

• ¬ negazione della formula atomica

• ∧ congiunzione

• ∨ disgiunzione

• 𝑎 ⇒ 𝑏 implicazione, composta da antecedente (𝑎) e conseguente (𝑏)

• 𝑎 ⇔ 𝑏 equivalenza

(in ordine di precedenza)

Logica proposizionale: semantica

La proposizione atomica T𝑟𝑢𝑒 è vera in ogni modello e Fals𝑒 è falsa in

ogni modello

Il valore di verità delle proposizioni atomiche deve essere specificato dal

modello

Per le formule complesse posso usare le tabelle di verità:

KB del mondo del Wumpus

Definisco dei simboli per ogni posizione presenza del 𝑃𝑥,𝑦 pozzo, 𝑊𝑥,𝑦

wumpus, 𝐵𝑥,𝑦 brezza, 𝑆𝑥,𝑦 fetore

Cosa sappiamo dopo aver visitato due stanze:

• ¬𝑃1,1 : non ci sono pozzi in [1,1]

• 𝐵1,1 ⟺ (𝑃1,2∨ 𝑃2,1) : se c’è brezza in [1,1] allora c’è un pozzo in [1,2]

o in [2,1]

• 𝐵2,1 ⟺ (𝑃1,1∨ 𝑃2,2 ∨ 𝑃3,1)

• ...

• ¬𝐵1,1 : non c’è brezza in [1,1]

• 𝐵2,1: c’è brezza in [2,1]

Vorremmo dimostrare che ¬𝑃2,2 (non ci sono pozzi in [2,2])

Enumerazione dei modelli

Ogni modello è un assegnamento di valori di verità alle proposizioni atomiche: solo tre assegnamenti rendono vera la KB

Proposizioni della KBProposizioni Atomiche

Non possiamo concludere che non c’è un pozzo in [2,2]

Ricerca sulla tavola di verità

Algoritmo: faccio una ricerca sugli assegnamenti con backtraking

• L’algoritmo è corretto: implementa la definizione di conseguenza

logica

• L’algoritmo è completo: funziona su ogni KB e formula, termina

sempre perchè il numero di configurazioni è finito

• Complessità temporale: 𝑂 2𝑛 con 𝑛 formule atomiche

• Complessità spaziale: 𝑂 𝑛 usando il backtracking

Dimostrazione di Teoremi

Grosso problema si verifica se il numero di modelli validi è molto grande

Posso provare a dimostrare teoremi, potrebbe essere più efficiente se la

lunghezza della dimostrazione è contenuta

Definisco che due formule 𝛼 e 𝛽 sono logicamente equivalenti 𝛼 ≡ 𝛽 se

sono vere nello stesso insieme di modelli

Definisco che una formula è valida se è vera in ogni modello (è anche

detta tautologia)

Definisco una formula soddisfacilibile se esiste almeno un modello in cui

essa è vera (SAT problem)

Teorema di deduzione:

Date 𝛼 e 𝛽, 𝛼 ⊨ 𝛽 se e solo se la formula 𝛼 ⟹ 𝛽 è valida

Equivalenze logiche

Inferenza e Dimostrazioni

Modus ponens𝛼 ⟹ 𝛽, 𝛼

𝛽

Tavola di verità:

Eliminazione degli and𝛼 ∧ 𝛽

𝛽

𝜶 𝜷 𝛼 ⟹ 𝛽

Vero Vero Vero OK

Vero Falso Falso OK

Equivalenze ed inferenza

Tutte le equivalenze possono essere usate come regole di inferenza

Ad esempio: eliminazione del bicondizionale

𝛼 ⟺ 𝛽

𝛼 ⟹ 𝛽 ∨ (𝛽 ⟹ 𝛼),𝛼 ⟹ 𝛽 ∨ (𝛽 ⟹ 𝛼)

𝛼 ⟺ 𝛽

Esempio (voglio dimostrare che non c’è un pozzo in [1,2]):

𝐵1,1 ⟺ (𝑃1,2∨ 𝑃2,1)

𝐵1,1 ⟹ (𝑃1,2∨ 𝑃2,1) ∨ ((𝑃1,2∨ 𝑃2,1) ⟹ 𝐵1,1)

(𝑃1,2∨ 𝑃2,1) ⟹ 𝐵1,1¬𝐵1,1⟹¬(𝑃1,2 ∨ 𝑃2,1) (contrapposizione)

¬(𝑃1,2 ∨ 𝑃2,1) (Modus ponens e percezione ¬𝐵1,1)

¬𝑃1,2 ∧ ¬𝑃2,1

Processo automatico di inferenza

La dimostrazione precedente è stata derivata a mano ma possiamo

vedere il problema come un problema di ricerca

• Stato iniziale: base della conoscenza

• Azioni: insieme delle regole di inferenza che si possono applicare (la

parte superiore corrisponde ad una delle regole presenti nella

conoscenza attuale)

• Transizione: aggiungo la parte inferiore della regola di inferenza alla

conoscenza attuale

• Obbiettivo: stato che contiene la formula che cerchiamo

Il tutto funziona perchè abbiamo la proprietà di monotonia: se traiamo

nuove conclusioni non possiamo invalidare ciò che abbiamo dimostrato

prima

Completezza della dimostrazione di formule

Proprietà dell’algoritmo di ricerca:

• Ottimalità: possiamo mettere passi unitari per ogni inferenza ed

utilizzare un algoritmo ottimo per arrivare alla dimostrazione più

veloce

• Completezza: dipende dalle regole di inferenza disponibili

Risoluzione: unita ad un algoritmo di ricerca completo rende la ricerca di

formule completa

Idea se 𝛼 ∨ 𝛽 ∨ 𝛾 e so che ¬𝛾 allora 𝛼 ∨ 𝛽

Risoluzione

Risoluzione unitaria:𝑙1 ∨ … ∨ 𝑙𝑘 , 𝑚

𝑙1 ∨ …∨ 𝑙𝑖−1 ∨ 𝑙𝑖+1 ∨ …∨ 𝑙𝑘

dove 𝑙𝑖 e 𝑚 sono letterali complementari

Risoluzione:𝑙1 ∨ … ∨ 𝑙𝑘 , 𝑚1 ∨ …∨𝑚𝑛

𝑙1 ∨ … ∨ 𝑙𝑖−1 ∨ 𝑙𝑖+1 ∨ …∨ 𝑙𝑘 ∨ 𝑚1 ∨ … ∨𝑚𝑗−1 ∨ 𝑚𝑗+1 ∨ …∨𝑚𝑛

dove 𝑙𝑖 e 𝑚𝑗 sono letterali complementari

(i letterali ripetuti vengono eliminati)

Applicabilità della formula di risoluzione

Sembrerebbe che la formula di risoluzione possa essere usata solo nel

caso in cui la KB sia formata da congiunzioni di clausole

Clausal Normal Form (CNF)

• Elimino i se e solo se con la congiunzione di due implicazioni

• Elimino le implicazioni

• Muoviamo all’interno le negazioni (con De Morgan)

• Distribuiamo gli and sugli or

Dimostrare una formula con risoluzione

Per dimostrare che 𝐾𝐵 ⊨ 𝛼, cerco di capire se 𝐾𝐵 ∧ ¬ 𝛼 è

insoddisfacibile (dimostrazione per contraddizione)

• Converto 𝐾𝐵 ∧ ¬ 𝛼 in CNF

• Applico risoluzione ad ogni coppia di formule con clausole

complementari

• Continuo finchè

• Non posso aggiungere altre clausole, quindi 𝛼 non è

conseguenza logica di 𝐾𝐵

• La risoluzione dà come risultato una clausola vuota, quindi 𝛼 è

conseguenza logica di 𝐾𝐵 (ho una contraddizione)