EPITA
Introdution à Prolog, cours n° 3 (suite)
Un programme de résolution propositionnelle
- Représentation de la forme clausale en Prolog
- Principe
- Exemples
- Gestion
des ensembles (listes) de clauses
- Normalisation
- Adjonction
sans duplication
- L'opération
centrale de la résolution
- Réduire
- Recherche d'une
résolvante
- Organisation
du processus global de résolution directe
- L'opérateur
de Robinson = un pas de résolution
- Le
processus de résolution
- Le
prédicat resoudre(Ref, LCl, LRes)
- Mise
en œuvre
- Réfutation
d'une forme clausale
- Traitement
des bases de règles pour moteurs d'inférences
- Réalisation de la
résolution linéaire
- Réalisation de la
SLD-résolution
- La
résolution simplifiée à la Prolog
- Application aux
bases
de règles pour moteurs d'inférences
-
Une proposition est représentée comme un ensemble (liste) de clauses
représentant la conjonction de ses membres.
Chaque clause est représentée par un couple d'ensembles (listes)
d'atomes,
- la première contient les atomes des littéraux négatifs
(donc, les antécédents des séquents de l'algorithme de Wang)
- la seconde les littéraux positifs (les conséquents des
séquents)
- La proposition de l'exemple précédent donne donc,
d'abord dans une
écriture hybride
[[[¬p]⋁[q]]⋀
[[¬q]⋁[r]]⋀
[[¬r]⋁[s]]⋀
[[¬t⋁¬s]⋁[]]⋀
[[]⋁[p]]⋀ [[]⋁[t]]]
puis en "vrai" Prolog :
[[[p],[q]], [[q],[r]], [[r],[s]], [[t,s],[]],
[[],[p]], [[],[t]]]
- De cette façon, la formule calculée plus haut par
l'algorithme de Wang
se lit :
[[[b], [d, a]], [[a], [d, c]], [[], [b, c]], [[f], []]]
= (¬b⋁d⋁a)⋀(¬a⋁d⋁c)⋀(b⋁c)⋀¬f, identique à la
donnée, comme annoncé.
- Le complexe de la girafe
(¬herbivore ⋁
girafe ⋁ buffle⋁ antilope) ⋀
(¬herbivore ⋁
¬félin) ⋀ (¬panthère ⋁
félin) ⋀
(¬tacheté ⋁
panthère ⋁ girafe) ⋀ herbivore ⋀ tacheté ⋀
¬girafe
s'écrit en Prolog :
[[[herbivore], [girafe,
buffle, antilope]],
[[herbivore, félin],
[]], [[panthère], [félin]],
[[tacheté], [panthère,
girafe]], [[], [herbivore]], [[], [tacheté]],
[[girafe],
[]] ]
-
-
Les clauses seront considérées comme normalisées, c'est-à-dire que
les
littéraux sont ordonnés en ordre standard fourni
par Prolog, via le prédicat 'sort'.
/* normalise(DonneeBrute, ResultatNormal) */
normalise([], []).
normalise([[N, P]|S], [[NN, NP]|NS]) :- sort(N, NN), sort(P, NP),
normalise(S,NS).
-
d'une liste d'objets
L1
(clauses ou atomes) à une autre liste d'objets L2
:
le prédicat standard union
de SWI-Prolog est valable puisque nos listes représentent des
ensembles.
Nous aurons aussi à nous assurer qu'un objet ne figure pas dans un
ensemble, ce pourquoi nous ferons appel au prédicat standard member.
-
Étant donné
X et Y
deux listes de littéraux de signes opposés,
trouver si elles ont un élément commun U,
et l'éliminer pour obtenir NX
et NY.
Si on échoue, c'est qu'il n'y a pas d'atome commun, donc pas de
résolution possible dans ce cas.
Emploi caractéristique de append
(prédicat standard correspondant à concat
amplement exemplifié dans ce cours)
pour
décomposer X et Y.
reduire(X, Y, NX, NY) :- append(AX, [U|DX],
X),
append(AY, [U|DY], Y),
append(AX, DX, NX), append(AY, DY, NY).
-
Le prédicat '
reduire' sert de test.
On essaie successivement les deux cas de figure "littéral négatif dans
la
première clause", "id. dans la seconde".
resolvante([NA, PA], [NB, PB], [NR,
PR]) :-
reduire(NA, PB, NNA, NPB), !,
% négatif
dans A
union(NNA,
NB, NS), add(NPB, PA, PS),
sort(NS,
NR), sort(PS, PR).
resolvante([NA, PA], [NB, PB], [NR, PR]) :-
reduire(PA, NB, NPA, NNB), !,
% négatif
dans B
union(NNB,
NA, NS), add(NPA, PB, PS),
sort(NS,
NR), sort(PS, PR).
-
(ainsi nommé d'après son inventeur, John
Alan Robinson)
- à partir d'une liste de clauses
LCl,
on calcule
- la liste
LR de toutes les
résolvantes nouvelles
des clauses de LCl
avec elles-mêmes.
Si cette liste est vide, on en conclut que LCl
est fermée par résolution (il n'y a plus de nouvelle résolvante).
robinson(LCl, LR) :- resoudre(LCl, LCl, LR).
Reste à définir le prédicat resoudre,
voir plus loin.
-
On itère l'opérateur de Robinson
jusqu'à
- soit trouver la clause vide
[[], []],
auquel cas "oui" la liste de clauses donnée est
contradictoire,
- soit ne plus engendrer de nouvelles résolvantes
(fermeture
par résolution),
auquel cas "non" la liste donnée n'est pas
contradictoire.
resolution(LCl) :- member([[],[]], LCl),
!,
write(oui).
resolution(LCl) :- robinson(LCl, LR), sresolution(LCl, LR).
sresolution(LCl, []) :- !, write(non). /* LCl fermee par resolution */
sresolution(LCl, LR) :- append(LR, LCl, L), resolution(L).
-
calcule
LRes
la liste des résolvantes de la liste LCl
avec elle-même qui ne sont pas dans Ref.
La liste Ref reste fixe, initialement
c'est la liste LCl elle-même (appel
à resoudre(LCl, LCl, LR)),
de manière à garantir qu'on ne retient que les résolvantes qui ne sont
pas dans LCl.
On procède
par recurrence sur LCl, en
itérant un prédicat 'resol(Ref, Cl, LCl, U)',
qui calcule dans LU la liste des
résolvantes nouvelles de LCl avec une
clause Cl.
resoudre(Ref, [], []).
resoudre(Ref, [Cl | SCl], LRes):- resol(Ref, Cl, SCl, LU), % la clause
Cl ne se résout pas contre elle-même !
resoudre(Ref, SCl, LS), union(LU, LS, LRes).
resol(Ref, Cl, [], []). % Résolvantes d'une clause avec une liste de
clauses
resol(Ref, Cl, [P|LS], LT) :- resolvante(Cl, P, R), !, sresol(Ref, R,
Cl, LS, LT).
resol(Ref, Cl, [_|LS], LU) :- resol(Ref, Cl, LS, LU).
sresol(Ref, R, Cl, LS, LR) :- member(R, Ref), !, resol(Ref, Cl, LS,
LR). % resol relancé sur la suite en oubliant R
sresol(Ref, R, Cl, LS, [Res|LR]) :- resol(Ref, Cl, LS, LR). %
resol relancé sur la suite en gardant R
-
On se dote d'un prédicat de commodité :
rresoudre(LCl) :- normalise(LCl, X), resolution(X).
?- rresoudre([[[p],[q]],
[[q],[r]], [[r],[s]], [[t,s],[]], [[],[p]], [[],[t]]]).
oui
true ;
false.
?- rresoudre([[[b], [d, a]],
[[a], [d, c]], [[], [b, c]], [[f], []]]).
non
true ;
false. ?- rresoudre([[[herbivore],
[girafe, buffle, antilope]],
| [[herbivore, félin], []],
[[panthère], [félin]],
| [[tacheté], [panthère,
girafe]], [[], [herbivore]], [[], [tacheté]],
| [[girafe], []] ]).
oui
true ;
false.
?- rresoudre([[[herbivore],
[girafe, buffle, antilope]],
[[herbivore, félin], []], [[panthère], [félin]],
[[tacheté], [panthère, girafe]], [[], [herbivore]], [[],
[tacheté]],
[[panthère], []] ]).
non
true ;
false.
winst([[[],[p]], [[],[u]],[[p],[q]],
[[q],[r]],
[[r],[s]],[[u,s],[]]]).
myst([[[p],[q]], [[q],[r]], [[r],[s]],
[[t,s],[]],
[[],[p]], [[],[t]]]).
hunt([ [[],[q]], [[],[p,r]], [[p],[s]],
[[r],[s]],
[[p,q,s],[]],[[q,r,s],[]] ]).
lovld([ [[],[a]], [[a],[b]], [[],[b,d]],
[[],[c,d]],
[[d],[c]],[[c],[e]], [[c,e],[]] ]).
nonex([ [[],[a,b,c]], [[],[e]], [[e],[b]],
[[],[r,s]] ]).
nyst([[[p],[q]], [[q],[r]], [[s],[r]],
[[u,s],[]],
[[],[p]], [[],[u]]]).
-
cf. notes de cours n° 2.
Les bases de règles de nos moteurs d'inférences d'ordre 0 sont des
clauses de Horn, donc des clauses !
Mais elles sont représentées en Prolog d'une manière plus économique
(nous allons y revenir).
Pour les traiter par le système de résolution général, il faut les
convertir.
Une base de règles ayant été lue (p. ex. :-[quadcomp].)...
lregcl([], []).
lregcl([[T|Q]|R], [[Q,[T]]|C]) :- lregcl(R,C).
lfaitcl([], []).
lfaitcl([F|SF], [[[], [F]]|C]) :- lfaitcl(SF, C).
clauses(SCl) :- bagof(R, regle(R), BR), lregcl(BR, RCl),
bagof(F,
fait(F), BF), lfaitcl(BF, FCl),
append(RCl,FCl, SCl).
regp(LButs) :- clauses(SCl), normalise([[LButs,
[]]|SCl],
LC), resolution(LC).
Mais notre procédure est beaucoup trop inefficace pour
traiter toute la base quadcomp.pl !
Essayons plutôt quadred.pl
regle([carre, rectangle, losange]).
regle([rectangle, parallelogramme, un_angle_droit]).
regle([parallelogramme, diag_milieu]).
regle([losange, parallelogramme, diag_ortho]).
regle([losange, quatre_cotes_egaux]).
fait(diag_milieu).
fait(diag_ortho).
fait(un_angle_droit).
et demandons
?- regp([carre]).
oui
true ;
false.
Le littéral resolin(Ref, Cl, LCl) réussit ssi il
dérive la
clause vide en résolvant linéairement LCl,
avec Cl comme clause initiale, en ne gardant
que les résolvantes qui ne sont pas dans Ref.
Procède par récurrence sur LCl,
sans cut de manière pouvoir explorer toutes
les possibilités par backtrack.
resolin(LRef, Cl, [P|LS]) :-
resolvante(Cl, P,
R), sresolin(LRef, R, Cl, LS).
resolin(LRef, Cl, [_|LS]) :- resolin(Ref, Cl, LS).
% et si LS est vide, échec de resolin, qui va provoquer un backtrack
dans "tresolin"
sresolin(LRef, [[], []], Cl, LS):- !, write(oui)
.
% Résolvante vide, on a
réussi
sresolin(LRef, R, Cl, LS) :- member(R, LRef), !, resolin(LRef,
Cl, LS).
/* Résolvante déjà connue, on relance sur la suite
*/
sresolin(LRef, R, Cl, LS) :- resolin([R|LRef], R,
[R|LRef] ).
/* Appel
récursif essentiel de la résolution linéaire */
tresolin(LRef, []) :- write(non), !. % échec
tresolin(LRef, [Prem|Suite]) :- resolin(LRef, Prem, Suite), !. %
backtrack sur échec de resolin
tresolin(LRef, [Prem|Suite]) :- tresolin(LRef, Suite).
reslineaire(LCl) :- tresolin(LCl, LCl).
rreslineaire(LCl) :- normalise(LCl, X), reslineaire(X).
/* pour essais à partir des bases de règles */
regl(LButs) :- clauses(SCl), normalise([[LButs,
[]]|SCl],
LC),
reslineaire(LC).
Exécution :
?- rreslineaire([[[herbivore], [girafe, buffle,
antilope]],
| [[herbivore, félin], []], [[panthère],
[félin]],
| [[tacheté], [panthère, girafe]], [[],
[herbivore]], [[], [tacheté]],
| [[girafe], []] ]).
true.
?- rreslineaire([[[herbivore], [girafe, buffle, antilope]],
[[herbivore, félin], []], [[panthère], [félin]],
[[tacheté], [panthère, girafe]], [[], [herbivore]], [[], [tacheté]],
[[panthère], []] ]).
false.
-
Le prédicat-maître est
reshorn(LButs, LClauses, LRef,
AncButs),
lancé par reshorn(LButs, LClauses,
LRef, LRef),
où
reshorn([B|SButs], [[B|Q]|SCl], LRef,
AncButs)
:-
union(Q,SButs,NButs),
sreshorn(NButs, [B|SButs], SCl, LRef, AncButs).
reshorn(LButs, [_|SCl], LRef, AncButs) :-
reshorn(LButs, SCl, LRef, AncButs).
sreshorn([], LButs, SCl, LRef, AncButs) :- !.
/* Liste de buts vide = Resolvante vide,
on a fini */
sreshorn(NButs, LButs, SCl, LRef, AncButs) :-
present(NButs, AncButs), !,
reshorn(LButs, SCl, LRef, AncButs).
sreshorn(NButs, LButs, SCl, LRef, AncButs) :- /* write(NButs), nl, */
reshorn(NButs, LRef, LRef,
[NButs|AncButs]).
[B|SButs]
et une clause [B|Q] (où B
est interprété comme positif), produisant la
résolvante (négative) NButs .
Comme aucune résolution ne sera possible dans l'avenir entre
elle et une future résolvante courante (qui sera toujours négative),
il est inutile de l'ajouter à l'ensemble de clauses LRef,
contrairement à ce qui se fait dans le cas général
(clause "sresolin(LRef, Res, Cl, Suite) :- resolin([Res|LRef],
Res, LRef).").
En revanche, il est essentiel de noter qu'on l'a traitée, pour
éviter de boucler.
D'où l'argument suplémentaire AncButs.
Le seul degré de liberté est le choix de la construction de la
résolvante,
qui doit réaliser la réunion des listes d'atomes (littéraux
négatifs) SButs et de la queue de
clause Q.
La stratégie Prolog de recherche en profondeur (la résolvante étant
gérée comme une pile)
se traduit par union = append et elle
entraîne des bouclages intempestifs.
La méthode correcte est de faire une union
sans duplication,
il faut donc recourir au prédicat add et à la
normalisation,
version simplifiée du predicat "resolvante" de
la résolution générale.
Exemples
ref1([[p], [u], [q,p,u], [r,q], [s,r]]).
but1([u,s]).
ref2([[q,p], [p,q], [r,q], [s,r], [p], [u]]).
but2([u,s]).
essaih1 :- ref1(R), but1(B), write('Horn'), resh(B,R), write('OK'), nl.
essaih2 :- ref2(R), but2(B), write('Horn'), resh(B,R), write('OK'), nl,
write('Prolog'), respg(B,R), write('FINI').
Exécution :
?- essaih1.
HornOK
true .
?- essaih2.
HornOK
true .
-
L'interprète Prolog gère la résolvante comme une pile, et
ne mémorise pas les résolvantes précédentes,
d'où un programme beaucoup plus simple, mais qui a une forte
tendance a boucler,
resprol(LButs, LRef, LCl)
resprol([], LRef, LCl) :- !.
resprol([B|SButs], LRef, [[B|Q]|SCl]) :-
/* sans "cut" car on peut avoir plusieur clauses de même tête*/
append(Q,
SButs, NButs), resprol(NButs, LRef, LRef).
resprol(LButs, LRef, [_|SCl]) :- resprol(LButs, LRef, SCl).
/* Appel par...*/
respg(LButs, LCl) :- resprol(LButs, LCl, LCl).
essaip1 :- ref1(R), but1(B), write('Prolog'), respg(B,R), write('FINI').
essaip2 :- ref2(R), but2(B), write('Prolog'), respg(B,R),
write('FINI').
Exécution :
?- essaip1.
PrologFINI
true .
?- essaip2.
Prolog
ERROR: Out of local stack
Exception: (285,353) resprol([q], [[q, p], [p, q], [r, q], [s, r], [p],
[u]], [[q, p], [p, q], [r, q], [s, r], [p], [u]]) ? creep
Exception: (285,352) resprol([p], [[q, p], [p, q], [r, q], [s, r], [p],
[u]], [[p, q], [r, q], [s, r], [p], [u]]) ? creep
Exception: (285,350) resprol([q], [[q, p], [p, q], [r, q], [s, r], [p],
[u]], [[q, p], [p, q], [r, q], [s, r], [p], [u]]) ? creep
Exception: (285,349) resprol([p], [[q, p], [p, q], [r, q], [s, r], [p],
[u]], [[p, q], [r, q], [s, r], [p], [u]]) ? creep
Exception: (285,347) resprol([q], [[q, p], [p, q], [r, q], [s, r], [p],
[u]], [[q, p], [p, q], [r, q], [s, r], [p], [u]]) ? abort
% Execution Aborted
?-
-
Cette fois la mise en œuvre est directe !
Il suffit de récupérer les règles qui ont été compilées à la lecture de
la base de règles...
Une base de règles ayant été lue (p. ex. :-[quadcomp].)...
Pour vérifier qu'une liste d'hypohèses a bien pour conéquences une
liste de buts :
regh(LButs, LHyp) :- setof(C, regle(C), R),
append(R, LHyp, RC), % par la résolution SLD
resh(LButs, RC).
regpg(LButs, LHyp) :- setof(C, regle(C), R), append(R, LHyp, RC), % par
la résolution Prolog
respg(LButs, RC).
Exécution, avec
regle([carre, rectangle, losange]).
regle([rectangle, parallelogramme, un_angle_droit]).
regle([parallelogramme, diag_milieu]).
regle([losange, parallelogramme, diag_ortho]).
regle([losange, quatre_cotes_egaux]).
?- regh([carre], [[diag_milieu], [diag_ortho],
[un_angle_droit]]).
true ;
true ;
false.
?- regpg([carre], [[diag_milieu], [diag_ortho], [un_angle_droit]]).
true ;
true ;
false.
Mais si on ajoute "regle([rectangle, carre])."
en tête de la base de règles...
?- regle([rectangle, carre]).
true .
?- regh([carre], [[diag_milieu], [diag_ortho], [un_angle_droit]]).
true .
?- regpg([carre], [[diag_milieu], [diag_ortho], [un_angle_droit]]).
ERROR: Out of local stack