Programmazione Logica -- Lezione 3

Corrispondenza fra semantica Dichiarativa e Operazionale

 La semantica operazionale definita nella scorsa lezione ha una relazione molto stretta con la semantica dichiarativa. Vediamo prima il caso ground:
Teorema (Correttezza)
Sia P un programma, e A un atomo ground.
Se <- A |-->* o (refutazione), allora M(P) |= A (o equivalentemente P |= A).
Teorema (Completezza)
Sia P un programma, e A un atomo ground.
Se M(P) |= A (o equivalentemente P |= A), allora <- A |-->* o.
Questi risultati mostrano che, almeno nel caso ground, le derivazioni corrispondono a corretti procedimenti deduttivi, e permettono di dimostrare tutte le conseguenze logiche.

In programmazione logica, pero', non sono solo gli atomi ground che ci interessano: piu' in generale, ci interessa trovare per quali valori un atomo e' consequenza logica, cioe' calcolare la una cas. I seguenti risultati generalizzao la correttezza e completezza della semantica operazionale al caso non ground.

Teorema (Correttezza generalizzata)
Sia P un programma, e A un atomo (non necessariamente ground).
Se <- A |-sigma->* o, allora P |= forall (A sigma) (dove forall (B) indica la chiusura universale di B).
Teorema (Completezza generalizzata)
Sia P un programma, A un atomo, e sigma una sostituzione.
Se P |= forall (A sigma), allora esiste theta piu' generale di sigma tale che <- A |-theta->* o.
Si ricorda che theta piu' generale di sigma se e solo se esiste una sostituzione phi tale che sigma = theta phi.
Notare che per il teorema di completezza generalizzata non basta considerare il modello minimo di Herbrand, ma occorre un'ipotesi su tutti i modelli di P . Infatti, per atomi non ground, il modello minimo non basta a caratterizzare la proprieta' di essere conseguenza logica.

Esempio: Albero genealogico

 Il seguente programma e' composto da un database che definisce le relazioni di padre e madre (notare che la linea di dicendenza e' maschile), e da clausole che definiscono le relazioni di genitore, antenato, fratello_sorella (cioe': fratello o sorella), fratellastro_sorellastra, e zio_zia. Per poter definire relazioni come fratello_sorella abbiamo bisogno di usare il predicato di disuguaglianza del Prolog X\=Y, che ha successo se e solo se X e Y non sono unificabili.

Programma:

padre(pippo,gino).
padre(luca,pippo).
padre(francesco,luca).
padre(pippo,manuela).
padre(luca,genoveffa).
padre(luca,giuseppina).

madre(giulia,gino).
madre(lina,pippo).
madre(gelda,luca).
madre(giulia,manuela).
madre(lina,genoveffa).
madre(franca,giuseppina).

genitore(X,Y) :- padre(X,Y).
genitore(X,Y) :- madre(X,Y).

antenato(X,Y) :- genitore(X,Y).
antenato(X,Y) :- genitore(X,Z), antenato(Z,Y).

fratello_sorella(X,Y) :-
padre(Z,X), padre(Z,Y), madre(W,X), madre(W,Y), X \= Y.
fratellastro_sorellastra(X,Y) :-
genitore(W,X), genitore(W,Y), X \= Y.
zio_zia(X,Y) :- genitore(Z,Y), fratello_sorella(X,Z).

Esempio di sessione:

Il Programma e' stato salvato in un file "Prog1.pl". Il seguente e' un esempio di sessione con l'interprete SWI-Prolog in cui si carica questo programma e si fanno delle query sulle relazioni madre, genitore, antenato, e fratello_sorella.

[cygnus:catuscia:~/Prolog:6] pl
Welcome to SWI-Prolog (Version 2.7.15)
Copyright (c) 1993-1996 University of Amsterdam. All rights reserved.

For help, use ?- help(Topic). or ?- apropos(Word).

1 ?- consult('Prog1').
Prog1 compiled, 0.01 sec, 2,772 bytes.

Yes
2 ?- madre(X,gino).

X = giulia ;

No
3 ?- madre(giulia,Y).

Y = gino ;

Y = manuela ;

No
4 ?- genitore(X,gino).

X = pippo ;

X = giulia ;

No
5 ?- antenato(X,gino).

X = pippo ;

X = giulia ;

X = luca ;

X = francesco ;

X = lina ;

X = gelda ;

No
6 ?- fratello_sorella(X,Y).

X = gino
Y = manuela ;

X = pippo
Y = genoveffa ;

X = manuela
Y = gino ;

X = genoveffa
Y = pippo ;

No
7 ?- halt.
[cygnus:catuscia:~/Prolog:7]