Termes et Atomes

Un terme est defini sur un ensemble de symboles de fonctions et de constantes :
si X est une variable alors X est un terme ; si c est une constante alors c est un terme ;
si f est un symbole de fonction et t1, . . ., tn sont des termes alors f(t1,. . .,tn) est un terme.
Un atome est defini sur un ensemble de symboles de predicats :
si p est un symbole de pr´edicats et t1, . . ., tn sont des termes alors p(t1,. . .,tn) est un atome.

Programme en clauses de Horn

Le langage des programmes de la programmation logique en clauses de Horn : l’ensemble des clauses d´efinies. Une clause d´efinie est constitu´ee dans cet ordre :
d’une tˆete de clause (un atome)
du symbole “ :-” (“si”)
d’un corps de clauses, conjonction d’atomes s´epar´es par le symbole “,”
le symbole “.”.
“Socrate est empoisonn´ si Socrate boit la cigu¨e et la cigu¨e est un poison.”
empoisonne(socrate): −
boit(socrate, cigue),
poison(cigue).
boit(socrate, cigue), poison(cigue) est le corps et empoisonne(socrate) est la tˆete de cette clause d´efinie.
Si le corps est absent, une clause d´efinie est un fait et est constitu´ee : d’une tˆete de clause (un atome)
le symbole “.”.
“Socrate est un homme.”
homme(socrate).
Un ensemble fini de clauses d´efinies (une conjonction) ayant le mˆeme nom de pr´edicat dans la tˆete en est sa d´efinition.
Variables logiques
Une variable logique repr´esente une donn´ee quelconque mais unique.
homme(X) signifie que l’“entit´ X est un homme”.
Une substitution est une fonction (un ensemble de couples Xi ← ti ) des variables dans les termes not´ee [X1 ← t1, . . . , Xn ← tn] (Xi distincte de ti et Xi toutes distinctes entre-elles).

La substitution vide (l’identit´e) est notee ǫ.

La substitution σ est ´etendue aux termes (et aux atomes) :
si (X ← t) ∈ σ alors σ(X ) = t sinon σ(X ) = X ; σ(f (t1, . . . , tn)) = f (σ(t1), . . . ,σ(tn )).
Le r´esultat de l’application d’une substitution σ (constitu´ee de couples Xi ← ti ) a` un terme (ou un atome) t, nomm´ee instance de t et not´ee σ(t), est le terme t dont toutes les occurrences des Xi ont et´ remplac´ees simultan´ement par les ti .

La substitution est associative mais non commutative.

La variable logique n’est pas un emplacement m´emoire et la substitution n’est pas une affectation.
Pour σ = [X ← socrate, Y ← platon] et t = ami (X , Y ) alors σ(t) = ami (socrate, platon).
Clauses Universelles et variables du programme
Dans une clause (ou un fait), la variable logique exprime que la clause (ou le fait) est vrai pour n’importe quelle donn´ee.
“Pour toute donn´ee X , si X est un homme alors X est mortel.” mortel(X) :- homme(X).
“Pour toute donn´ee X , si X est mortelle et X est empoisonn´ee alors X meurt.”
meurt(X) :- mortel(X), empoisonne(X).
Les variables sont locales et g´en´eriques (elles sont renomm´ees a` chaque utilisation).
Les variables peuvent aussi bien ˆetre utilis´ee en entr´ee qu’en sortie.

Prolog, le langage

Le programme de la mort de Socrate
animal(X) :- homme(X).
mortel(X) :- animal(X).
meurt(X) :-
mortel(X), empoisonne(X).
empoisonne(X) :-
boit(X,Y), poison(Y).
homme(socrate).
homme(platon).
ami(socrate, platon).
ami(platon, socrate).
boit(socrate, cigue).
poison(cigue).

L’unification

L’unification calcule une substitution qui rend des termes ´egaux.
Soient E = {t1, . . . , tn} un ensemble de termes et σ une substitution.
σ unifie E si par d´efinition σ(t1) = . . . = σ(tn) (σ est un unificateur de E et E est unifiable).
L’unificateur σ d’un ensemble de termes E est l’unificateur le plus g´en´eral (upg) de E si quelque soit σ′ un unificateur de E il existe une substitution η telle que σ′ = ση.
Deux termes unifiables admettent un unique unificateur le plus g´en´eral (au renommage des variables pr`es).
Notation :
σ({t1 = t1′, . . . , tn = tn′}) =
{σ(t1) = σ(t1′), . . . , σ(tn) = σ(tn′)}

Algorithme d’unification (Martelli-Montanari)

Initialisation : θ0 = ǫ et E0 = {tj = tj′}1≤j≤n.
R´esultat : l’upg de {tj = tj′}1≤j≤n s’il existe Tant que Ei n’est pas l’ensemble vide,
(1) si Ei = {f (s1, . . . , sp) = f (s1′, . . . , sp′ )} ∪ Ei′ alors
Ei +1 = {sj = sj′}1≤j≤p ∪ Ei′ et θi +1 = θi ;
(2) si f (s1, . . . , sp ) = g (s1′, . . . , sm′) ∈ Ei avec
f = g ou p = m alors arrˆet de la boucle avec ´echec ;
(3) si Ei = {X = X } ∪ Ei′ alors Ei +1 = Ei′ et θi +1 = θi ;
(4) si (Ei = {t = X } ∪ Ei′ ou Ei = {X = t} ∪ Ei′), t = X
et X V (t) alors Ei +1 = [X ← t](Ei′) et θi +1 = θi [X ← t] ;
(5) si (Ei = {t = X } ∪ Ei ou Ei = {X = t} ∪ Ei ),
t = X et X ∈ V (t) alors arrˆet de la boucle avec ´echec.

Questions existentielles

Dans une question, la variable logique exprime une interrogation sur l’existence d’une donn´ee qui v´erifie le pr´edicat.
“Existe-t-il une donn´ee X telle que X soit mortelle ?”
? mortel (X )
La r´eponse `a une question existentielle est constructive (non uniquement existentielle) et collecte les instanciations pour les variables qui sont des solutions.
? mortel (X )
[X ← socrate]
La question peut ˆetre une conjonction d’atomes. . .
homme(socrate).
homme(platon).
ami(socrate,platon).
ami(platon,socrate).
“Existe-t-il une donn´ee X et une donn´ee Y telles que X soit ami de Y et X soit un homme ?”
? ami (X , Y ), homme(X )
et la r´eponse multiple.
[X ← socrate][Y ← platon]
[X ← platon][Y ← socrate]

Semantique operationnelle

La r`egle de d´erivation SLD :
B1, . . . , Bi −1, Bi , Bi +1, . . . , Bp C , i σ(B1, . . . , Bi −1,θ(A1), . . . ,θ(An), Bi +1, . . . , Bp)
si C = (A : −A1, . . . , An) ∈ P,
V (θ(A : −A1, . . . , An)) ∩ V (B1, . . . , Bp) = ∅,
σ ∈ upg (θ(A), Bi ).
B1, . . . , Bp est une r´esolvante et θ une substitution de renommage.
Deux degr´es de libert´ :
– le choix de l’atome a` r´eduire ;
– le choix de la clause pour r´eduire.
L’unification est l’unique m´ecanisme de passage de param`etres.
Une d´erivation SLD de r´esolvante initiale R0, la question, est une suite finie ou infinie (Rj )j≥0 de r´esolvantes telle que
Rj Cj , ij
Rj+1
Une succ`es ou r´efutation SLD d’une r´esolvante R0 est une d´erivation finie (Rj )0≤j≤r telle que la derni`ere r´esolvante est vide.
Une d´erivation telle que la derni`ere r´esolvante ne peut plus inf´erer de nouvelle r´esolvante est une d´erivation ´echec.
1
z }| {
meurt(X )
mortel(X1), empoisonne(X1) C0 ,1∈{1}
avec C0 = meurt(X ) : −mortel(X ), empoisonne(X ).
et θ0 = [X ← X1] et θ0(meurt(X )) = meurt(X1)
et donc σ0 = upg (meurt(X1), meurt(X )) = [X ← X1]
σ0(θ0(mortel(X )), θ0(empoisonne(X ))) = mortel(X1), empoisonne(X1).
1 2
z }| { z }| {
mortel(X1), empoisonne(X1)
mortel(X2), boit(X2, Y2), poison(Y2) C1 ,2∈{1,2} avec C1 = empoisonne(X ) : −boit(X , Y ), poison(Y ).
θ1 = [X ← X2][Y ← Y2] et θ1(empoisonne(X )) = empoisonne(X2) et donc σ1 = upg (empoisonne(X2), empoisonne(X1)) = [X1 ← X2] σ1(mortel(X1), θ1(boit(X , Y )), θ1(poison(Y ))) =
mortel(X2), boit(X2, Y2), poison(Y2).
1 2 3
z }| { z }| { z }| {
mortel(X2), boit(X2, Y2), poison(Y2)
animal(X3), boit(X3, Y2), poison(Y2) avec C2 = mortel(X ) : −animal(X ).
et θ2 = [X ← X3] et θ2(mortel(X )) = mortel(X3) et donc σ2 = upg (mortel(X3), mortel(X2)) = [X2 σ2(θ2(animal(X )), boit(X2, Y2), poison(Y2)) = animal(X3), boit(X3, Y2), poison(Y2).
C2,1∈{1,2,3}
← X3]
1 2 3
z }| { z }| { z }| {
animal(X3), boit(X3, Y2), poison(Y2)
animal(X3), boit(X3, cigue) C3 ,3∈{1,2,3}
avec C3 = poison(cigue).
et θ3 = ǫ
et donc σ3 = upg (poison(cigue), poison(Y2)) = [Y2 ← cigue] σ3(animal(X3), boit(X3, Y2)) = animal(X3), boit(X3, cigue).

1 Introduction
2 Programmation Logique
3 Prolog, le langage