Sistemi e schedulazione in tempo reale E.Mumolo [email protected].
AGENTI CHE RAGIONANO LOGICAMENTE E.Mumolo [email protected].
-
Upload
giulia-pasquali -
Category
Documents
-
view
225 -
download
3
Transcript of AGENTI CHE RAGIONANO LOGICAMENTE E.Mumolo [email protected].
AGENTI CHE RAGIONANO LOGICAMENTE
Un agente basato sulla conoscenza deve: Conoscere lo stato del mondo Conoscere come il mondo cambia nel tempo Saper fare inferenze per decidere le proprie azioni
L’agente conosce il mondo attraverso una base della conoscenza (KB)
La base della conoscenza è espressa mediante un Linguaggio formale chiamato Logica
La logica è formata da Sintassi = proposizioni ammissibili del linguaggio Semantica = verità di una proposizione (significato)
Agenti basati sulla conoscenza
Base di conoscenza
Motore inferenziale
Base di conoscenza
Algoritmi indipendenti dal dominio
Contenuto specifico del dominio
• Base di conoscenza (Knowledge Base o KB). Un insieme di rappresentazioni relative ad aspetti del mondo espresso in formule di un Linguaggio di rappresentazione della conoscenza.
• Livello dell’implementazione
• strutture dati
• algoritmi per manipolarle
Logica
• La logica è un linguaggio formale per rappresentare delle informazioni e per trarre delle conclusioni
• La sintassi definisce le proposizioni ammissibili del linguaggio
• La semantica definisce il “significato” delle proposizioni cioè la verità di una proposizione in un mondo
Es. il linguaggio dell’aritmetica:
x + 2 >= y è una proposizione
x2 + y > non è una proposizione
x + 2 >= y e’vera se e solo se x+2 non è minore di y
x + 2 >= y è vera in un mondo dove x = 7, y = 1
x + 2 >= y è falsa in un mondo dove x = 0, y = 6
Il mondo è visto secondo questi oggetti
Tipi di logica
Quello che un agente crede degli oggetti del mondo
Linguaggio
• Differenti tipi di logiche
Logica Proposizionale Fatti vero/falso/sconosciuto
Logica del prim'ordine Fatti, oggetti, relazioni vero/falso/sconosciuto
Logica temporale Fatti, oggetti, relazioni, tempi vero/falso/sconosciuto
Teoria delle probabilità Fatti noti secondo livelli di probabilità
Logica Fuzzy Fatti noti secondo gradi di appartenenza
Definizione di teoria assiomatica
Alfabeto (insieme finito di simboli) Stringa (sequenza di simboli) Fbf=Formule ben formate (sottoinsieme di stringhe) Assiomi (sottoinsieme di fbf) Regole di Inferenza (da insiemi di fbf nuove fbf)
Deve esistere un algoritmo per decidere se Una stringa è una fbf Una fbf è un assioma Una generica fbf è ricavabile da un insieme di fbf
Dimostrazione: sequenza finita di fbf Teorema: l’ultima fbf di una dimostrazione
Sintassi
Inoltre
Altre definizioni:
Definizione di teoria assiomaticaSemantica
Interpretazione: Alle fbf ed ai simboli delle fbf è associato un insieme di significati
Definizione di fbf vera Proprietà della inferenza:
fbf vere fbf vere
Modello di una teoria assiomatica: interpretazione per cui tutti gli assiomi della teoria sono veri
Corollario: i teoremi della teoria fbf veri
Ma: fbf vera in ogni modello della teoria) teorema? NON in generale
Ci sono fbf vere in ogni modello che non sono dimostrabili!
Componenti della Logica Proposizionale
Proposizioni: una qualunque espressione in lingua italiana (o inglese) di cui si possa dire se è vera o falsa Es. “303 è pari” “303” “esiste una soluzione a 3x=10” …
Compito della logica: Conoscere il valore di una proposizione dati i valori delle sue componenti Esaminare come dalla veritò di alcune proposizioni si possa derivare la
verità di altre proposizioni NON è stabilire se e perché sono vere e false!
Connettivi logici ~ negazione implicazione, equivalenza congiunzione disgiunzione ≡ uguaglianza ( ) parentesi
PROPOSIZIONI: una qualunque espressione di cui si possa dire se è vera o falsa
CONNETTIVI LOGICI:~ negazione, implicazione equivalenza,
congiunzione, disgiunzione, ≡ uguaglianza,
FORMULE BEN FORMATE == forme proposizionali (fp) REGOLA DI INFERENZA Modus Ponens (MP):
Da A e AB consegue B ASSIOMI. Se A,B,C sono fp, si possono condensare in tre forme
generali: A1 : (A(BA)); A2: ((A(BC))((AB)(AC))) A3 : ((~B ~A)((~BA)B))
Componenti della Logica Proposizionale
Componenti della Logica Proposizionale
Implicazione e equivalenza Implicazione: . Indica la formula (~)
Falsa solo quando è vera e è falsa. Equivalenza: Indica la formula
( (~) ) ( (~) )
Vera se e solo se e hanno gli stessi valori di verità.
Riepilogo delle Forme proposizionali
Le fbf della logica proposizionale sono forme proposizionali (fp)
Definizione ricorsiva: Ogni simbolo di proposizione è una fp Se A e B sono fp, lo sono anche
~A, AB, AB, A B, A B, A ≡ B
ASSIOMI. Se A,B,C sono fp, si possono condensare in tre forme generali:
A1 - (A(BA))A2 - ((A(BC))((AB)(AC)))A3 - ((~B ~A)((~BA)B))
Inferenza Regola di inferenza Modus Ponens (MP):
Da A e AB consegue B
Esempio: dimostrazione che DD (D è una fp)Partiamo da A1 - (A(BA))e A2 - ((A(BC))((AB)(AC)))Con A=D, B=(DD), C=D si ha:
(D((DD)D))((D((DD)D))((D(DD))(DD)))
Applichiamo MP a queste due fp. Si ha: § ((D(DD))(DD))D’altra parte, da A1 con A=D e B = DD =D si ha §§ (D(DD))Applichiamo MP a § e §§. Si ha (DD). (dimostrazione del Teorema)
Semantica
Simbolo di proposizione valore Vero/Falso Tabella di verità dei connettivi logici
A B ~A AB A B A B A ≡ B
V V F V V V VV F F F F V FF V V V F V FF F V V F F V
Abbreviazioni
I connettivi logici , , ≡ abbreviano alcune fp: (A B) abbrevia (~(A(~B)))
(A B) abbrevia ((~A)B)
(A ≡ B) abbrevia ((AB)
Infatti:
A B ~A ~B A B A B A ≡ B A B B A (A(~B)) (~A)B (AB)
V V F F V V V V V F V V
V F F V F V F F V V V F
F V V V F V F V F V V F
F F V F F F V V V V F V
Tautologie
Una tautologia è una fp vera sotto ogni interpretazione Esempio: gli assiomi sono tautologie. Infatti per il primo e terzo:
TeoremaOgni tautologia è un teorema
CorollarioOgni teorema è decidibile (tavola di verità con 2n
interpretazioni e n simboli)
A B ~A ~B A B B A(A(BA))
(primo assioma)
(~B ~A) (~B A) ((~BA)B)) ((~B ~A)((~BA)B))(terzo assioma)
V V F F V V V V V V V
V F F V F V V F V F V
F V V F V F V V V V V
F F V V V V V V F V V
Tautologie (esempio)
Proposizione: “se o piove o c’è il sole, e non piove, allora c’è il sole” Dimostrazione semantica: la traduco in fbf e verifico se è una
tautologia Fbf: ((P S) ~P) S
P S ~P P S (P S) ~P (P S) ~PS
V V F V F VV F F V F VF V V V V VF F V F F V
Componenti della Logica Proposizionale
Secondo riepilogo delle Forme proposizionali
PROPOSIZIONI: una qualunque espressione di cui si possa dire se è vera o falsa
CONNETTIVI LOGICI:
~ negazione, implicazione equivalenza,
congiunzione, disgiunzione, ≡ uguaglianza,
FORMULE BEN FORMATE == forme proposizionali (fp)
REGOLA DI INFERENZA Modus Ponens (MP): Da A e AB consegue B
ASSIOMI. Se A,B,C sono fp, si possono condensare in tre forme generali: A1 : (A(BA)); A2: ((A(BC))((AB)(AC))) A3 : ((~B ~A)((~BA)B))
Un Teorema è l’ultima fbf di una dimostrazione
Secondo riepilogo delle Forme proposizionali (cont.) Tabella di verità: enumera tutte le possibili interpretazioni della fp (n simboli
2n interpretazioni)
Gli assiomi sono tautologie.
Dimostrazione semantica: tabella di verità
Teorema: Ogni tautologia è un teorema
Corollario: Ogni teorema è decidibile (tavola di verità )
Una tautologia è una fp vera sotto ogni interpretazione.
Dimostrazione sintattica: sequenza finita di fbf a partire dagli assiomi e tautologie
Dimostrazione automatica di teoremi
Tautologie notevoli della Logica Proposizionale
Prop. Commutativa a b ≡ b a a b ≡ b a
Prop. Associativa (a b) c ≡ a b c) (a b) c ≡ a b c)
Prop. Distributiva a b c) ≡ (a b) (a c) a b c) ≡ (a b) (a c)
De Morgan 1,2: ~(a b) ≡ (~a ~b ); ~(a b) ≡ (~a ~b )
Contrapposizione a b ≡ ~b ~a
Risoluzione unitaria Da ~b e (a b) segue a
Eliminazione di Congiunzione a b a a b b (da a e b deriva a o b)
Aggiunta di Disgiunzione a a b b a b(da a o b deriva a b)
Esercizi
Dimostrare semanticamente e sintatticamente che
(~x ~(y ~z)) x ~(y z)) ≡ ~x ~y ~z Semanticamente:
Sintatticamente:(~x ~(y ~z)) x ~(y z)) ≡ (x (~y z)) ~x (~y ~z)) ≡~(x (~y z)) ~x (~y ~z)) ≡ ~(x ~y z) ~x ~y ~z) ≡(~x y ~z) ~x ~y ~z) ≡ (~x ~x ~y ~z) (y ~x ~y ~z) (~x ~x ~y ~z) ≡(~x ~y ~z) (~x ~y ~z) ≡ ~x ~y ~z
x 0 0 0 0 1 1 1 1
y 0 0 1 1 0 0 1 1
z 0 1 0 1 0 1 0 1
(~x ~(y ~z)) x ~(y z)) 1 1 1 1 1 1 1 0
Esercizi
Dimostrare sintatticamente e semanticamente che
(x ~(y z)) (x (y z)) è una tautologia
Semanticamente:
(x ~(y z)) (x (y z)) ≡ ~ (x (~y ~z)) (x (y z)) ≡
(~x ~(~y ~z)) (x (y z)) ≡ (~x (y z)) (x (y z)) ≡
~x (y z) (x (y z) ≡ (~x x) (y z) ≡ ~x xSemanticamente:
x 0 0 0 0 1 1 1 1
y 0 0 1 1 0 0 1 1
z 0 1 0 1 0 1 0 1
(x ~(y z) (x (y z)) 1 1 1 1 1 1 1 1
Verificare la seguente equivalenza: (a b) ~(a c) ≡ ~(a bc)
Per definizione: indica la formula (~) quindi
(a b) ~(a c) ≡ ~ (a b) ~(a c) ≡ per De Morgan: (~A ~B ) ≡ ~(A B) ≡ ~( (a b) (a c) ) ≡ ~( a b a c ) ≡ prop. Commutativa ≡ ~( a a b c ) ≡ ~( a b c )
Verificare se la fp (ab) ((a~b) ~a) è una tautologia(ab) ((a~b) ~a) per def. ≡ (~a b) ((~a ~b) ~a) ~(~a b) (~(~a ~b) ~a) ≡ ~(~a b) ( (a b) ~a) ≡ (a ~b) ((a b) ~a) ≡ (distributiva) (a ~b) ((a ~a)b ~a) ≡(a~b)b~a) ≡ (commutativa) (a~b)~ab) ≡ (DeMorgan) (a~b)ab) ≡ Vero
D’altra parte, con la tabella di verità
A B (A B ) (A~B) ( B) ~A ) fp
V V V F V V
V F F V F V
F V V V V V
F F V V V V
Esercizi
Dimostrare il seguente teorema:Se (c b) a (Prima Ipotesi ) e ~b (Seconda ipotesi ) allora: a
Dimostrazione:1- (c b) a prima ipotesi2- (c a) (b a) prop. Distributiva3- (b a) Eliminazione di congiunzione4- ~b a Equivalenza logica a (3)b seconda ipotesi6- a M.Ponens da (5) e (4)
Altra dimostrazione:1- ~ b seconda ipotesi2- ~ b (~ b ~ c) Aggiunta di disgiunzione3- ~ b ~ c M. Ponens da (1) e (2)4- ~(b c) De Morgan a (3)5- (c b) a prima ipotesi6- ~(c b) a equiv. logica a (5)7- a M. Ponens da (4) e (6)
Esercizi
Dimostrare il seguente teorema:Da (~a (b c)) (prima ipotesi) e (~a ~b) (seconda ipotesi) deriva c
Dimostrazione:(1) ~a ~b Ipotesi 2(2) ~a eliminazione di congiunzione(3) ~a (b c) Ipotesi 1(4) b c M. Ponens da (2) e (3)(5) ~ b c Definizione di implicazione (4)(6) ~ b Eliminazione di congiunzione da (1)(7) c M. Ponens da (5) e (6)
Nota: la tesi si trova solo nella conseguenza della 1a ipotesi un buon candidato è MP.
Esercizi
Dimostrare informalmente il seguente teorema:Da (a b c) (prima ipotesi) e (a b) c (seconda ipotesi) deriva c
La seconda ipotesi dice che c, la tesi, puo essere dedotta dalla proposizione(a b). La prima ipotesi, dice che c puo essere dedotta da ~(a b). Quindi, si può dire che c e vera indipendentemente dalla veridicita di a b.Quindi la tesi è vera per ogni possibile valore di a b.
Esercizi
Dimostrare il seguente teorema:Da a (prima ipotesi) e (~a c) ~b (seconda ipotesi) si deduce ~b.
Dimostrazione:(1) (~a c) ~b ipotesi 2(2) ~ (~a c) ~b Definizione di implicazione (1)(3) (a ~c) ~b De Morgan (2)(4) a ipotesi 1(5) a ~c Introd. di disgiunzione (4)(6) ~b Modus Ponens da (3) e (5)
Esercizi
Esempio: il robot Cartesiano CART Scopo: CART si muove in un ambiente. NON deve investire le
persone ma DEVE raccogliere del materiale Scenario:
Il mondo è diviso in caselle CART può muoversi solo secondo gli assi cartesiani, di casella in casella Ci sono delle caselle dove ci sono persone: CART non deve andare in quelle
caselle per motivi di sicurezza! Ci sono caselle con pavimento scivoloso: CART si perde in quelle caselle!
Percezioni: CART ha tre sensori S,P,M con i quali percepisce che:
S: Un quadrante adiacente in direzione orrizzontale o verticale è scivoloso
P: In un quadrante adiacente in orrizzontale o verticale c'è una persona
M: Nel quadrante attuale c'è materiale da raccogliere
Azioni: gira sinistra, gira destra, avanza, prendi
Inoltre: P! = c'è una persona, S!= pavimento scivoloso, OK = cella sicura.
V = cella visitata
1,4 2,4 3,4 4,4
1,3 2,3 3,3 4,3
1,2 2,2 3,2 4,2
4,13,12,11,1 A
OK OK
OK
1,4 2,4 3,4 4,4
1,3 2,3 3,3 4,3
1,2 2,2 3,2 4,2
4,13,12,11,1
OK S, OK
OK
V S ?
S ?
OK
V
OK
Alcuni passi di esplorazione...
Percezioni1,1
=[- - -] → (2,1) e (1,2) OK → vado in (2,1)
A
1,4 2,4 3,4 4,4
1,3 2,3 3,3 4,3
1,2 2,2 3,2 4,2
4,13,12,11,1
OK OK
OK
A
V V
Percezioni1,2
=[- P -] → (1,3) e (2,2) NON sicureMa 2,2 non P e non S → vado in (2,2)
a b
c
Percezioni2,1
=[S - -] → (2,2) e (3.1) NON OK→ vado in (1,2)
Ad ogni passo: L’agente percepisce l’ambiente Aggiunge le percezioni alla KB
La visita delle celle (1,1) (2,1) e (1,2) fornisce le seguenti percezioni: ~P1,1 ~S1,1
~P2,1 S2,1
P1,2 ~S1,2
Posizione persona: conoscenza racchiusa in 3 regole: R1: ~P1,1 ~P!1,1 ~P!1,2 ~P!2,1
R2: ~P2,1 ~P!1,1 ~P!2.1 ~P!2,2 ~P!3,1
R3: P1,2 P!1,3 P!1,2 P!2,2 P!1,1
Esempio: il robot Cartesiano CART
Cosa deve fare l’agente? Deve dimostrare dov'è la persona! Dalla KB non è in (1,1) (1,2) (2,1) (2,2) (3,1) L’agente si chiede se è in (1,3). Quindi deve dimostrare la tesi P!1,3
Dimostrazione semantica: 212 possibilità (12 variabili) Dimostrazione sintattica: applicando inferenza!
procedimento meccanico! (automatizzabile)1. ~P!1,1 ~P!1,2 ~P!2,1 (M.Ponens con ~P1,1 e R1)2. ~P!1,1 ~P!1,2 ;~P!2,1 (eliminazione di disgiunzione)
Analogamente si ottiene:1. ~P!2,2 ~P!2,1 ;~P!3,1 (M.Ponens con ~P2,1 e R2 e elim.di disgiun.)
2. (P!1,3 P!1,2 P!2,2) P!1,1 (MP con P1,2 e R3, associat.)
3. (P!1,3 P!1,2 ) P!2,2 (Risoluzione unitaria e 2., associat.)4. (P!1,3 P!1,2 ) (Risoluzione unitaria e 3.)5. P!1,3 (Risoluzione unitaria e 3.)
CVD
Esempio: il robot Cartesiano CART
d
1,4 2,4 3,4 4,4
1,3 2,3 3,3 4,3
1,2 2,2 3,2 4,2
4,13,12,11,1
OK OK
OK
A
V V
V
Percezioni2,2
=[- - -] → (3,2) e (2,3) sicure → vado in (2,3)
Esempio: il robot Cartesiano CART
Continua l'esplorazione in 2,2:
Percezioni2,3
=[S P M] → RACCOLGO MATERIALEContinua l'esplorazione in 2,3:
• Alla fine della esplorazione, CART si accorge che l'ambiente era il seguente:
1,4 2,4 3,4 4,4
1,3 2,3 3,3 4,3
1,2 2,2 3,2 4,2
4,13,12,11,1
start cellascivolosa
cellascivolosa
cellascivolosa
P
P
P, M, S
S S
S
S
S(S!)
(S!)
(S!)
(P!)
Esempio: il robot Cartesiano CART
Problemi dell’agente proposizionale Non riesce facilmente a rispondere a domande del tipo:
“cosa devo fare adesso?” esempio “non andare avanti se c’è una persona di fronte a te”
Non è impossibile, ma diventa troppo complesso: Per il robot cartesiano CART, ho 64 regole. Deve avere conoscenza del passato, es. 100 passi: 6400 regole!
Dovrei avere regole del tipo A1,1 Verso_Est W2,1Avanti
Dovrei avere variabili che rappresentano situazioni logica del prim’ordine: può ridurre 6400 regole a 1
Limiti della logica proposizionale (I)
Le regole che abbiamo scritto devono essere ripetute per ogni quadrato e per ogni orientamento dell’agente.
Se consideriamo una griglia 4*4 e 4 diverse orientazioni dell’agente abbiamo 4*4*4=64 copie della stessa regola.
Un secondo problema riguarda il tempo. Se per t = 0 l’agente
è in [1,1] e vale al tempo t = 1 andrà dimenticato
mentre sara vero se l’agente si sposta in quel quadrato. Dobbiamo cioè tenere conto del tempo.
Dovremo ricorrere a una logica più ricca: la logica dei predicati del primo ordine.
Limiti della logica proposizionale (II)
Logica dei predicati del primo ordineLa logica dei predicati del primo ordine permette di rappresentare:
•Oggetti: persone, cose, numeri etc.
•Relazioni: fratello, maggiore, parte di etc.
•Proprietà: rosso, primo, grande etc.
•Funzioni: successore, somma, padre di etc.
Esempi:
“Uno più due uguale tre” - uno,due,tre sono oggetti, più è una funzione, uguale è una relazione
“Il diabolico Re Giovanni imperversò in Inghilterra nel 1200”
Giovanni, Inghilterra e 1200 sono oggetti, imperversò è una relazione, re e diabolico sono proprietà
•Simboli di variabile: x, y, z
•Simboli di costante: A,B,C,Giovanni
•Simboli di predicato: Tondo, Fratello
•Simboli di funzione: Padre_di, Quadrato
•I soliti connettivi logici più la virgola più le parentesi ( )
•Il quantificatore esistenziale
•Il quantificatore universale Termini: variabile o costante o simbolo di funzione
Formule atomiche: fbf formata da un simbnolo di predicato seguito da una lista di termini es:
Fratello(Riccardo,Giovanni)
Sposati(Madre_di(Riccardo),Padre_di(Riccardo))
Logica dei predicati del primo ordine: sintassi
Formule complesse:
si ottengono dalle formule atomiche usando i connetivi logici
,,,~,
)30,(~)30,(
)30,()30,(
),(),(
GiovanniPiùGiovaneGiovanniPiùGrande
LuigiPiùGiovaneGiovanniPiùGrande
RiccardoGiovanniFratelloGiovanniRiccardoFratello
Logica dei predicati del primo ordine: sintassi
Per dare un significato a una formula bisogna interpretarla come una affermazione sul dominio del discorso.
Un dominio D è un insieme non vuoto (anche infinito) ad es. Insieme di persone, l’insieme dei naturali etc.
Una interpretazione si ottiene associando
•ad ogni simbolo variabile un elemento di D
•ad ogni simbolo costante un elemento di D
•ad ogni simbolo di funzione una funzione su D
•ad ogni predicato n-ario una relazione n-aria su D
Ad ogni formula atomica si assegna un valore vero o falso
Ad ogni formula complessa si assegna un valore vero o falso utilizzando le tavole di verita
Logica del primo ordine: semantica
Esempio di interpretazione
Sia data la formula P(a,f(b,c))
Una possibile interpretazione è:
D è il dominio degli interi
•a è l’intero 2
•b è l’intero 4
•c è l’intero 6
•f è la funzione addizione
•P è la relazione maggiore di
Questa formula ha valore falso
Se a è l’intero 11 la formula assume valore vero
Logica del primo ordine: semantica
)0,()(
)0,100(...)0,2()0,1()0,0(
xPx
PPPP
Quantificatore universale:
supponiamo che P sia la relazione MaggioreUguale
Quantificatore esistenziale:
supponiamo che Q sia una qualche proprietà
)()(
)...()()(
xQx
cQbQaQ
Logica del primo ordine: variabili e quantificatori
)()()()(~
)()()()(~
eequivalenz segeunti le Valgono
x)a dipende esiste chey elemento(l'
),())((
),())((
annidati toriQuantifica
xWxxWx
xWxxWx
yxPyx
yxPyx
Logica del primo ordine: variabili e quantificatori
),(
:inferisce si
),(),(
:da
y)),Genitore(px)(p,p)Genitore(yxy)o(x,y)(Fratell(x,
c)),Genitore(pp)(g,p)Genitore(c),c)(Nonno(g(g,
p)Figlio(c,c)(p,c)Genitore(p,
c),Genitore(mFemmina(m)c)c)Madre(m,(m,
PARENTELE
LucaMarioFratello
LucaGiovanniGenitoreMarioGiovanniGenitore
Logica dei predicati del primo ordine
Assiomi di una teoria del prim’ordine
Stessi della logica proposizionale
A1 - (A(BA))A2 - ((A(BC))((AB)(AC)))A3 - ((~B ~A)((~BA)B))
Poi:A4 – più tardiA5 - ((x)(AB)(A((x)B)))
Poi:
A6… gli assiomi propri della teoria
Assiomi di una teoria del prim’ordine
Regole di inferenza MP: da A e AB segue B Generalizzazione: da A segue ((x)(A)
Abbreviazioni; Stesse della logica proposizionale:
(A B) abbrevia (~(A(~B))) (A B) abbrevia ((~A)B) (A ≡ B) abbrevia ((AB)
Poi: ((x)A) abbrevia (~(((x)(~A)))
Esempio di teoria del prim’ordine
Teoria elementare dei numeri: Assiomi propri della teoria:
A6 - x1=x2 (x1=x3x2=x3)A7 - x1=x2 x1+1 = x2+1A8 - 0 (x1)+1A9 - (x1)+1=(x2)+1 x1=x2A10 - x1+0=x1A11 - x1+(x2+1)=(x1+x2)+1A12 - x1-0=x1A13 - x1*(x2+1)=(x1*x2)+x1A14 - A(0) ((x)(A(x) A(x+1)) (x)A(x)) //principio di induzione
Esempio di teoria del prim’ordine
Teoria elementare dei numeri: alcuni teoremi:A6’ - t = r (t = s r = s)…A10’ - t+0=t… Teorema 10.1: t=t
Dim. t+0=t; i) (t+0=t) (t+0=t t=t); con MP (da A e AB consegue B):(t+0=t t=t); ii)con MP da i) e ii): t=t cvd
Teorema 10.1: t=r r=t Dim. da A6’: t=r (t=tr=t) i)
Applicando MP alla tautologia (t=r(t=tr=t)) (t=t(t=rr=t)) e a i): t=r (t=rr=t) ii)
Applicando MP a 10.1 e ii):t=r r=t cvd
Esempio di applicazione robotica
Dal Teorema di completezza (Goedel 1930):Se tutte le nostre conoscenze su un argomento possono essere messe in forma di assiomi, tutti i teoremi (conseguenze) possono essere ricavate meccanicamente
Problema generale: la conoscenza non è sempre assiomatizzabile!
Metodo di risoluzione meccanica di Robinson
Poi: esempio di problema robotico: Robot esapodo Raccogliere oggetti ad una certa altezza
Metodo di risoluzione di Robinson
Conoscenza assiomi
Riduciamo gli assiomiforma normale(x)(y)(P(y)~(y)(Q(x,y)P(y))) prima riduzione: (x)(y)(~P(y) ~(y)(~Q(x,y) P(y))) seconda riduzione: (x)(y)(~P(y) (y)(Q(x,y) ~ P(y))) cambiamo i nomi delle variabili se conflitti: (x)(y)(~P(y) (z)(Q(x,z) ~ P(z))) spostiamo i quantificatori: (x)(y) (z)(~P(y) (Q(x,z) ~P(z))) e usiamo la associatività: (x)(y) (z)((~P(y) Q(x,z)) ~P(y)~P(z)))cambiamo l-effetto di (z( con una funzione z=g(x,y): (x)(y) (~P(y) (Q(x, g(x,y)) ~P(y)~P(g(x,y))))FORMA Normale: {~P(y) (Q(x, g(x,y), ~P(y)~P(g(x,y)}
Dimostrazione del teorema per assurdo: Insieme di fbf formato da assiomi speciali, ipotesi, negazione del teorema
Formula ottenuta per risoluzione da due formule date: Sostituzione di argomenti per rendere i due predicati uguali e si unisce al resto
Metodo di Robinson: tutte le coppie di bfb vengono risolte e vengono aggiunte all’insieme di fbf. Se si ottiene una fbf vuota il teorema è dimostrato
Esempio: Robot esapodo
Il robot si muove in un mondo dove c’è una scatole e ci sono oggetti appesi ad una certa altezza
Gli oggetti possono essere presi solo se il robot sale sulla scatola Il compito del robot è di raccogliere tutti gli oggetti appesi Teorema: qual è la sequenza di operazioni? Problema: il robot cambia il mondo assiomi variabili (stato del mondo) Azioni possibili: muovere un oggetto, arrampicarsi, afferrare
Variabili; M (il robot) S(stato) B (oggettp) P(punto) Operatori
muovi(M,B,P,S) Arrampicati(M,B,S) Afferra(M.B,S)
Assiomi: descrivono lo stato del mondo Predicati:
mobile(x) se x può essere spostato In(x,y,S) Scalabile(x,y,S) Raggiungibile(x,y,S) Ha(x,y,S) Sopra(s,y,S)
Teorema: (S) Ha(robot,oggetto,S)
Dimostrazione ottenibile con Robinson: Lo stato cercato è ottenuto da S0 dopo che
il robot ha mosso la cassa sotto l’ oggetto, si e’ arrampicato sull cassa, ha afferrato l’oggetto
Esempio: Robot esapodo