Post on 11-Sep-2018
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
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)