FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

25
FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine

Transcript of FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

Page 1: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

FMZ

Linguaggi di ProgrammazioneDa logica proposizionale a logica del primo ordine

Page 2: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

FMZ

Logica proposizionale Sintassi vs Semantica

Sintassi Semantica Mondo

Concetto di modello

Funzione di interpretazione

SimboliFBFASSIOMIRegole di inferenza

S F S F

???

Page 3: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

FMZ

Una dimostrazione per

è una sequenza

DIM=P1,P2,…,Pn

• Pn=F• PiS• PiASSIOMI• Pi è ottenibile da Pi1,…,Pim (con i1<i,.., im<i)

applicando una regola di inferenza

Sintassi vs Semantica Osservazioni

S F

Page 4: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

FMZ

DIM=P1,P2,…,Pn

Problema: introduciamo sempre formule vere?• PiS vere per ipotesi

• PiASSIOMI veri poiché tautologie

• Pi è ottenibile da Pi1,…,Pim (con i1<i,.., im<i) applicando una regola di inferenza

Sintassi vs Semantica Osservazioni

anello debole

Page 5: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

FMZ

Sintassi vs Semantica Regole di inferenza e veridicità

VVFF

VFVF

A BVFVV

AB

VVFF

VFVF

A BVFFF

AB

P B , P

BMP

A1,…,An

A1… An

A1… An

Ai

AE

AI

Page 6: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

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)

Page 7: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

FMZ

Logica proposizionale (limiti)

Socrate è un uomo.Gli uomini sono mortali. (A)Allora Socrate è mortale.

Traduzione di (A) nella logica proposizionaleSe 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.

Page 8: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

FMZ

Logica del primo ordine(logica dei predicati del primo ordine)

SintassiIngredienti:

Simboli LL– LetteraliLetterali

• Costanti individuali Ai

• Variabili individuali i

• Lettere funzionali fi

• Lettere predicative Pi

– Connettivi LogiciConnettivi Logici: {,,,,(,)},

Page 9: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

FMZ

Logica del primo ordine Sintassi

Ingredienti:Termine TTermine 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 groundTermine ground - senza variabili (oggetti dell'Universo del discorso)Es.: padre(padre(giovanni))

Page 10: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

FMZ

Formule Atomiche (atomi)Formule Atomiche (atomi)

Se t1,…,tn T alloraPi(t1,…,tn) è una formula atomicaformula atomica

Logica del primo ordine Sintassi

Esempi: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))

Page 11: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

FMZ

Logica del primo ordine Sintassi

Ingredienti:Formule Ben FormateFormule Ben Formate

– Le Formule Atomiche sono FBF

– Se f1 e f2FBF e x è una variabile individuale allora

x.f1FBF

x.f1FBF

f1FBF

f1 f2FBF

f1 f2FBF

f1f2FBF

Page 12: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

FMZ

Logica del primo ordine Sintassi

Ingredienti:Regole di inferenzaRegole di inferenza

– Eliminazione del quantificatore universale

– Eliminazione del quantificatore esistenziale

– Introduzione del quantificatore esistenziale

x.F(…x…)SUBST({x/a},F(…x…)}

x.F(…x…)

SUBST({x/a},F(…x…)}

F(…a…)

x.F(…x…)

Dove a non appartiene a costanti già introdotte

Page 13: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

FMZ

1) un esempio filosofico(X)(uomo(X) mortale(X)) uomo(socrate) mortale(socrate)

2) due degli assiomi di base dei numeri naturaliinterpretare 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

Logica del primo ordine Sintassi esempiSintassi esempi

Page 14: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

FMZ

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.InterpretazioneInterpretazione (I):• Insieme DInsieme D (dominio)

I(ai) = di per ciascuna costante individuale

• Insieme di funzioni I(fi) = fi

fi: Dn D per ciascuna lettera funzionale fi

• Insieme di relazioniI(Pi)=Pi

Pi Dn per ciascuna lettera predicativa Pi

Logica del primo ordine SemanticaSemantica

Page 15: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

FMZ

Logica del primo ordine SemanticaSemantica

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

Page 16: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

FMZ

Logica del primo ordine SemanticaSemantica

Interpretazione• Interpretazione delle formule quantificateI(x.Pi(a1,…,x,…,an))=V se per tutti gli x D accade

che (I(a1),…,x,…,I(an))I(Pi)

=F altrimenti

I(x.Pi(a1,…,x,…,an)) =V se esiste x D tale che (I(a1),…,x,…,I(an))I(Pi)

=F altrimenti

Page 17: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

FMZ

una sostituzionesostituzione è un insieme finito della forma{v1 t1,…, vn tn}

vi è una variabileti è un termine diverso da vi

le variabili vi, i=1,…,n sono tra loro distinteuna sostituzione è una funzione da variabili a termini

l’applicazione di 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 E) è unaistanza di E.

Sostituzione

Page 18: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

FMZ

siano = {X1 t1,…, Xn tn} e = {Y1 u1,…, Ym um} due sostituzionila composizionecomposizione di e (denotata da ) è la sostituzione così definita

i) costruiamo l’insieme

{X1 t1,…, Xn tn, Y1 u1,…, Ym um}

ii) eliminiamo dall’insieme gli elementiXi titali che ti = Xi

iii) eliminiamo dall’insieme gli elementi Yj uj tali che Yj occorre in {X1,…, Xn}

Sostituzione: Composizione

Page 19: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

FMZ

= {X f(Y), Y Z} = {X a, Y b, Z Y}

costruzione di costruzione di 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 costruzione di 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}

Sostituzione: Composizione

Page 20: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

FMZ

L’unificazione è un meccanismo che permette di calcolare unasostituzione 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 è un unificatoreunificatore per {E1,…, Ek}se e solo se E1= E2 = …= EkUn insieme {E1,…, Ek} è unificabileunificabile se e solo se esiste una sostituzione tale che è un unificatore per {E1,…, Ek}ESEMPIOESEMPIO: l’insieme {p(a,Y), p(X,f(b))} è unificabile

dato che la sostituzione = {X a, Y f(b)} è un unificatore per l’insieme

Unificazione

Page 21: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

FMZ

• un unificatore per l’insieme {E1,…, Ek} èl’unificatore più generale (most generalunifier, mgu) se e solo se per ogni unificatore dell’insieme {E1,…, Ek} esiste unasostituzione tale che =

• esiste un algoritmo (algoritmo diunificazione), che, dato un insieme diespressioni E = {E1,…, Ek},

rivela la sua non unificabilità, oppurecalcola un unificatore più generale per E

Unificazione

Page 22: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

FMZ

Logica proposizionale vs. Logica del primo ordine

“Aggiunte”:

• Strutturazione dei letterali

• Introduzione delle variabili

• Introduzione dei quantificatori

Page 23: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

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}

Page 24: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

FMZ

Logica del primo ordine

Socrate è un uomo.Gli uomini sono mortali. Allora Socrate è mortale.

• Traduzione affermazioniUomo(Socrate)x.(Uomo(x) Mortale(x))

• Traduzione goalMortale(Socrate)

Page 25: FMZ Linguaggi di Programmazione Da logica proposizionale a logica del primo ordine.

FMZ

Logica del primo ordine

x.(Uomo(x) Mortale(x))

(SUBST({x/Socrate},Uomo(x) Mortale(x))

Universal Elimination

Uomo(Socrate) Mortale(Socrate) , Uomo(Socrate) MP

Mortale(Socrate)