Linguaggi di Programmazione
Da logica proposizionale
a logica del primo ordine
FMZ
Logica proposizionale
Sintassi vs Semantica
Sintassi
Semantica
Simboli
FBF
ASSIOMI
Regole di inferenza
Funzione di
interpretazione
S
F
S
???
Mondo
F
Concetto di
modello
FMZ
Sintassi vs Semantica
Osservazioni
Una dimostrazione per
S
F
è una sequenza
DIM=P1,P2,…,Pn
•
•
•
•
Pn=F
PiS
PiASSIOMI
Pi è ottenibile da Pi1,…,Pim (con i1<i,.., im<i)
applicando una regola di inferenza
FMZ
Sintassi vs Semantica
Osservazioni
DIM=P1,P2,…,Pn
Problema: introduciamo sempre formule vere?
• PiS
• PiASSIOMI
vere per ipotesi
veri poiché tautologie
• Pi è ottenibile da Pi1,…,Pim (con i1<i,.., im<i)
applicando una regola di inferenza
anello debole
FMZ
Sintassi vs Semantica
Regole di inferenza e veridicità
A1,…,An
A1… An
A1… An
Ai
PB,P
B
AI
A
V
V
F
F
B
V
F
V
F
AB
V
F
F
F
A
V
V
F
F
B
V
F
V
F
AB
V
F
V
V
AE
MP
FMZ
Sintassi vs Semantica
• La preservazione della veridicità è
osservabile per induzione
• Formalmente:
– (Meta)Teorema di completezza
– (Meta)Teorema di Deduzione (+ Ogni teorema
di L è una tautologia)
FMZ
Logica proposizionale (limiti)
Socrate è un uomo.
Gli uomini sono mortali. (A)
Allora Socrate è mortale.
Traduzione di (A) nella logica proposizionale
Se Gino è un uomo, allora Gino è mortale.
Se Pino è un uomo, allora Pino è mortale.
Se Rino è un uomo, allora Rino è mortale.
Se Socrate è un uomo, allora Socrate è mortale.
…
Se X è un uomo, allora X è mortale.
FMZ
Logica del primo ordine
(logica dei predicati del primo ordine)
Sintassi
Ingredienti:
Simboli L
– Letterali
•
•
•
•
Costanti individuali Ai
Variabili individuali ai
Lettere funzionali fi
Lettere predicative Pi
– Connettivi Logici: {,,,,(,)},
FMZ
Logica del primo ordine
Sintassi
Ingredienti:
Termine T
costanti individuali T
variabili individuali T
Se t1,…,tn T allora
fi(t1,…,tn) T (applicazione di un simbolo di funzione n-ario a n
termini)
Termine ground - senza variabili (oggetti dell'Universo del discors
Es.: padre(padre(giovanni))
FMZ
Logica del primo ordine
Sintassi
Formule Atomiche (atomi)
Se t1,…,tn T allora
Pi(t1,…,tn) è una formula atomica
Esempi: uomo(paolo)
maggiore(X,3)
maggiore(più(X,1),Y)
ama(giovanni,maria)
ama(padre(giovanni),giovanni)
ama(padre(padre(giovanni)),giovanni)
maggiore(più(più(1,giovanni),Y),padre(3))
FMZ
Logica del primo ordine
Sintassi
Ingredienti:
Formule Ben Formate
– Le Formule Atomiche sono FBF
– Se f1 e f2FBF e x è una variabile individuale allora
x.f1FBF
x.f1FBF
 f1FBF
f1 f2FBF
f1 f2FBF
f1f2FBF
FMZ
Logica del primo ordine
Sintassi
Ingredienti:
Regole di inferenza
– Eliminazione del quantificatore universale
x.F(…x…)
SUBST({x/a},F(…x…)}
– Eliminazione del quantificatore esistenziale
x.F(…x…)
Dove a non appartiene a costanti
già introdotte
SUBST({x/a},F(…x…)}
– Introduzione del quantificatore esistenziale
F(…a…)
x.F(…x…)
FMZ
Logica del primo ordine
Sintassi esempi
1) un esempio filosofico
(X)(uomo(X)  mortale(X))  uomo(socrate) 
mortale(socrate)
2) due degli assiomi di base dei numeri naturali
interpretare f e g come funzioni successore e predecessore
la costante
0 come zero il predicato u come uguaglianza )
(X)(Y)(u(Y,f(X))  (Z)(u(Z,f(X))  u(Y,Z)))
(X)( ~u(X,0) 
((Y)(u(Y,g(X))  (Z)(u(Z,g(X))  u(Y,Z)))))
3) nella formula (X) p(X,Y), tutte le occorrenze di X sono
vincolate, mentre Y è libera
FMZ
Logica del primo ordine
Semantica
Dare
una
interpretazione
alle
espressioni
sintatticamente corrette. Definire se certe espressioni
sono vere o false in base al significato che si dà ai
componenti
dell'espressione.
Interpretazione
(I):
•
Insieme D (dominio)
I(ai) = di
•
Insieme di funzioni
I(fi) = fi
fi: Dn  D
•
per ciascuna costante individuale
per ciascuna lettera funzionale fi
Insieme di relazioni
I(Pi)=Pi
Pi  Dn
per ciascuna lettera predicativa Pi
FMZ
Logica del primo ordine
Semantica
Interpretazione
• Interpretazione delle formule atomiche
– I(Pi(a1,…,an)) =V
se (I(a1),…,I(an))I(Pi)
=F
altrimenti
– I(x.Pi(a1,…,x,…,an)) =V
se per tutti gli x d accade che
(I(a1),…,x,…,I(an))I(Pi)
=F altrimenti
FMZ
Logica del primo ordine
Semantica
Interpretazione
• Interpretazione delle formule quantificate
I(x.Pi(a1,…,x,…,an))=V
=F
I(x.Pi(a1,…,x,…,an)) =V
=F
se per tutti gli x D accade
che (I(a1),…,x,…,I(an))I(Pi)
altrimenti
se esiste x D tale che
(I(a1),…,x,…,I(an))I(Pi)
altrimenti
FMZ
Sostituzione
una sostituzione J è un insieme finito della forma
{v1  t1,…, vn  tn}
vi è una variabile
ti è un termine diverso da vi
le variabili vi, i=1,…,n sono tra loro distinte
una sostituzione è una funzione da variabili a termini
l’applicazione di J ad E è l’espressione ottenuta da E
sostituendo simultaneamente ogni occorrenza della variabile
vi, i=1,…,n con
il termine ti il risultato dell’applicazione (denotato da EJ) è
una
FMZ
istanza di E.
Sostituzione: Composizione
siano J = {X1  t1,…, Xn  tn} e
l = {Y1  u1,…, Ym  um} due sostituzioni
la composizione di J e l (denotata da J  l) è la sostituzione
così definita
i) costruiamo l’insieme
{X1  t1l,…, Xn  tnl, Y1  u1,…, Ym  um}
ii) eliminiamo dall’insieme gli elementi
Xi  til tali che til = Xi
iii) eliminiamo dall’insieme gli elementi
Yj  uj tali che Yj occorre in {X1,…, Xn}
FMZ
Sostituzione: Composizione
J = {X  f(Y), Y  Z}
l = {X  a, Y  b, Z  Y}
costruzione di J  l
i)
{X  f(b), Y  Y, X  a, Y  b, Z  Y}
ii)
{X  f(b), X  a, Y  b, Z  Y}
iii)
{X  f(b), Z  Y}
costruzione di l  J
i)
{X  a, Y  b, Z  Z, X  f(Y), Y  Z}
ii)
{X  a, Y  b, X  f(Y), Y  Z}
iii)
{X  a, Y  b}
FMZ
Unificazione
L’unificazione è un meccanismo che permette di calcolare una
sostituzione al fine di rendere uguali due espressioni. Per
espressione intendiamo un termine, un letterale o una
congiunzione o disgiunzione di letterali.
Sia dato un insieme di espressioni (termini, atomi, etc.) {E1,…
Ek}
una sostituzione J è un unificatore per {E1,…, Ek}se e solo se
E1J = E2J = …= EkJ
Un insieme {E1,…, Ek} è unificabile se e solo se esiste
una sostituzione J tale che J è un unificatore per {E1,…,
Ek}
ESEMPIO: l’insieme {p(a,Y), p(X,f(b))} è unificabile dato che
la sostituzione J = {X  a, Y  f(b)} è un unificatore per
FMZ
l’insieme
Unificazione
• un unificatore J per l’insieme {E1,…, Ek} è
l’unificatore più generale (most general
unifier, mgu) se e solo se per ogni unificatore
l dell’insieme {E1,…, Ek} esiste una
sostituzione  tale che l = J  
• esiste un algoritmo (algoritmo di
unificazione), che, dato un insieme di
espressioni E = {E1,…, Ek},
rivela la sua non unificabilità, oppure
calcola un unificatore più generale per E
FMZ
Logica proposizionale vs. Logica
del primo ordine
“Aggiunte”:
• Strutturazione dei letterali
• Introduzione delle variabili
• Introduzione dei quantificatori
FMZ
Logica del primo ordine
Socrate è un uomo.
Gli uomini sono mortali.
Allora Socrate è mortale.
• Costanti individuali
{Socrate, Pino, Gino, Rino}
• Lettere predicative
{Uomo,Mortale}
FMZ
Logica del primo ordine
Socrate è un uomo.
Gli uomini sono mortali.
Allora Socrate è mortale.
• Traduzione affermazioni
Uomo(Socrate)
x.(Uomo(x)  Mortale(x))
• Traduzione goal
Mortale(Socrate)
FMZ
Logica del primo ordine
x.(Uomo(x)  Mortale(x))
Universal Elimination
(SUBST({x/Socrate},Uomo(x)  Mortale(x))
Uomo(Socrate)  Mortale(Socrate) , Uomo(Socrate)
MP
Mortale(Socrate)
FMZ