APPENDICE. Sintassi e semantica FOL (Firts Order Logic)
description
Transcript of APPENDICE. Sintassi e semantica FOL (Firts Order Logic)
APPENDICE. Sintassi e semantica FOL (Firts Order Logic)
• Comp(P) e’ una formula del primo ordine pieno. Richiamiamo sintassi e semantica per chi non avesse seguito logica. Ci limitiamo alle interpretazioni di Herbrandt.
LA SINTASSI di FOL:
Termine ::= Variabile | Costante | SimboloF(Termine,…,Termine)
Atomica ::= SimboloP(Termine,…,Termine)
Formula ::= Atomica | (not Formula) |
(Formula Formula) |
(Formula Formula) |
(Formula Formula) |
(Formula Formula) |
(Formula Formula) | (x Formula) |
(x Formula).
Esempio
Nei cortili ci sono solo cani e gatti, cioè se X è in un cortileè un cane o un gatto. Nel cortile corte3 ci sono un gatto e un cane.
x,c (incortile(x,c) cane(x) gatto(x)) a,b (cane(a) gatto(b) incortile(a,corte3) incortile(b,corte3))
Solite precedenze; i quantificatori hanno la precedenza di not
In prolog: le segnature% Segnatura corrente definita da una base dati con:% aconst(X) : X è una costante% avar(X) : X è una variabile% afunc(F,N) : F simbolo funzione N-ario% apred(P,N) : P simbolo predicato N-ario
avar(X) :- member(X,[a,b,c,x]).aconst(X) :- member(X,[felix,pluto,corte3]).apred(cane,1).apred(gatto,1).apred(incortile,2).
In prolog: le atomiche in una segnatura
aterm(X) :- aconst(X); avar(X); ( X =.. [F|Terms], afunc(F,N), terms(Terms,N) ).
anAtom(X) :- X =.. [P|Terms], apred(P,N), terms(Terms,N).
terms([],0).terms([T|TT],N) :- N > 0, M is N-1, aterm(T), terms(TT,M).
In prolog: le formule% uso operatori infissi:- op(200,xfy,&).:- op(220,xfy,v).:- op(150,fy,non).:- op(250,xfx,imp).:- op(250,xfx, se).:- op(250,xfx,sse).
aformula(X) :- anAtom(X); X = non A, aformula(A); X = A & B, aformula(A), aformula(B); X = A v B, aformula(A), aformula(B); X = A imp B, ….. X = exi(V,A), avar(V), aformula(A); X = for(V,A), avar(V), aformula(A).
Variabili libere
è detto quantificatore universale ed è detto quantificatore esistenziale
• In (Qx A), dove Q è un quantificatore, A è detta scopo di Qx
• Una variabile x occorre vincolata in una formula se occorre nello scopo di un quantificatore Qx; occorre libera se non occorre vincolata; può occorrere sia libera, sia vincolata.
• Una formula è chiusa se nessuna variabile occorre libera
• Le sostituzioni sostituiscono SOLO le occorrenze libere
• Le istanze chiuse o ground si ottengono sostituendo con termini ground tutte le occorrenze libere di variabili
X,C (incortile(X,C) cane(X) gatto(X)) vede(X,Y)
X quantificata X libera
(X,C (incortile(X,C) cane(X) gatto(X)) vede(X,Y)){X/fido}= (X,C (incortile(X,C) cane(X) gatto(X)) vede(fido,Y)
ESEMPIO
Le istanze ground nell’universo {fido,felix} sono 4:
(X,C (incortile(X,C) cane(X) gatto(X)) vede(fido,fido)(X,C (incortile(X,C) cane(X) gatto(X)) vede(fido,felix)(X,C (incortile(X,C) cane(X) gatto(X)) vede(felix,fido)(X,C (incortile(X,C) cane(X) gatto(X)) vede(felix,felix)
Sostituzione in Prolog
% La sostituzione distingue fra quantificatori e qualsiasi altro operatore;% conviene introdurre due decomposizioni in sottoespressioni:
quantified(QF,Q,V,Sub) :- F = [Q,V|Sub], member(Q,[for,exi]).
compound(F,Op,Sub) :- F ..= [Op|Sub], ( afunc(Op,_); apred(Op,_); aPropositrionalOp(Op) )
aPropositionalOp(X) :- member(X,[non, &, v, imp, se, sse])
Sostituzione in Prologsubst(X,S,T,Bounded) :- avar(X), % Bounded -> non sostituita member(X,Bounded) -> T=X; ( member(X/T1,S) -> T = T1; T = X ).subst(C,_,C,_) :- aconst(C).
subst(F,S,F1,BoundV) :- compound(F,Op,Sub), substlist(Sub,S,Sub1,BoundV), compound(F,Op,Sub1).
subst(QF,S,QF1,BoundV) :- quantified(QF,Q,V,Subf), substlist(Subf,S1,Subf1,[V|BoundV]), quantified(QF1,Q,V,Subf1).
substlist([X|L],S,[X1|L1],B) :- subst(X,S,X1,B), substlist(L,S,L1,B).substlist([],_S,[],_B).
Modelli di Herbrandt in Prolog
• Ci limitiamo al caso privo di funzioni; ci sono solo costanti, come in datalog. Usiamo:intp(Interp, [C1,…,Cn], [A1,..,An]) : C1,..,Cn è l’universo di Herbrandt dominio di Interp e A1,…,An sono tutti e soli i fatti veri in Interp
• Esempio:intp(caniegatti, [felix,fido], [vede(felix,fido), scappa(felix)]).
Verità in un modello di HerbrandtBase. A atomica chiusa:
H |= A sse A HPasso. • H |= A sse non H |= A • H |= A B sse H |= A e H |= B• H |= A B sse H |= A o H |= B• H |= x A sse H |= A per ogni istanza chiusa A • H |= x A sse H |= A per almeno un’istanza chiusa A
Nota. A B equivale a A BA B equivale a B A
A B equivale a (A B) (A B)
Esercizio Prolog
• Usando le rappresentazione e i predicati prolog definiti nei lucidi precedenti e messi nel file prolog allegato alla lezione, definire i seguenti predicati, dove V e’ una variabile, A,A1 sono formule chiuse e H e’ un’interpretazione di Herbrandt:
istanza(V/C,A,A1,H) : significa “A1 = A{V/C} per un C nel dominio di H”H /= A :
significa “A è vera in H”
Per la quantificazione universale si puo’ usare il predicato predefinito prolog forall come segue:forall(istanza(V/_,A,A1,H), vera(A1,H)).
Esempio
xy ( cane(x) incortile(x,y)) x (cane(x) abbaia(x))
È vera nella seguente interpretazione?
cane(pluto). Universo = {pluto,felix,c1}abbaia(pluto).gatto(felix).incortile(pluto,c1).
1. xy ( cane(x) incortile(x,y)) vero? 2. x (cane(x) abbaia(x)) vero?
cane(pluto). Universo = {pluto,felix,c1}abbaia(pluto).gatto(felix).incortile(pluto,c1).
Risolviamo 1. Scegliamo l’istanza x=pluto
y ( cane(pluto) incortile(pluto,y)) vero?
Scegliamo l’istanza y = c1
cane(pluto) incortile(pluto,c1) vero?
ora come nel proposizionale
1. xy ( cane(x) incortile(x,y)) vero? 2. x (cane(x) abbaia(x)) vero?
cane(pluto). Universo = {pluto,felix,c1}abbaia(pluto).gatto(felix).incortile(pluto,c1).
Risolviamo 2. Le istanze sono x=pluto, x=felix, x=c1
cane(pluto) abbaia(pluto) vero? cane(felix) abbaia(felix) vero? cane(c1) abbaia(c1) vero?
ora come nel proposizionale