EPITA
Introdution à Prolog, cours n° 2 : le second ordre en Prolog
- La négation
par l'échec
- La
primitive call
- La
négation
- Interprétation
- Analyse et synthèse
de
termes
- Analyse/synthèse
des termes par les prédicats spécialisés
- Le
prédicat très spécial "=.."
- Manipulation
de la base de connaissances
- Ajouter
un fait ou une clause: assert
- Supprimer
un fait ou une clause: retract
- Exemple : Un petit
lecteur-évaluateur interactif d'exp. arithmétiques
- Autre exemple de
l'emploi d'assert/retract : AZERTYOP.
- Les
prédicats setof et bagof
- setof(FormeInstance,
LittéralPrédicat,
EnsembleTrouvé)
- bagof(FormeInstance,
LittéralPrédicat,
ListeTrouvée)
- Questions
de Logique
- Moteurs
d'inférences, à l'ordre 0 strict
- Ordre 0
- Moteur
en marche arrière
- Moteur
en marche avant
- Module
d'explication, visualisant l'arbre de
preuve
- Exemple
: une base de connaissances relative aux quadrilatères
- Exécution
- Cryptarithmétique
élémentaire
- L'exemple
standard SEND+MORE = MONEY
- Généralisation
-
call(Terme) où Terme
est un littéral.
lance la résolution de Terme dans le
contexte courant
(analogue aux funcall et apply
de Lisp)
-
prédicat défini par
not(P) :- call(P) , !, fail.
not(P).
-
la négation par échec et l'hypothèse du monde clos : ce qui n'est pas
démontrable est réputé faux...
Exemple : not(pere(jules, X)) ne
cherche pas tous les X dont jules
n'est pas pere,
mais constate que jules a un fils, et
répond false
(il faut donc lire not(∃X pere(jules,X)),
contrairement à la pratique ordinaire ).
Le fond du problème est qu'une clause Prolog avec une variable libre
réussit dès qu'on a trouvé une valeur idoine,
donc s'interprète comme précédée d'un quantificateur existentiel, pas
universel !
- Exemple : le prédicat d'inclusion (selon
Deransart
& Ferrand)
inclus(L1, L2) :- not(ninclus(L1, L2)).
ninclus(L1, L2) :- elt(X, L1), not(elt(X, L2)).
elt(X, [X | L]) :- !.
elt(X, [Y | L]) :- elt(X, L).
- Commentaire : Oui ça marche, c'est même la
seule façon
de faire !
En effet, on sait tester la non-inclusion, puisque la variable
libre X est quantifiée
existentiellement,
mais pas l'inclusion, qui demanderait un quantificateur universel...
-
functor(Terme, Fonc, Arité)
arg(N°, Terme, Argt)
?- functor(la_mere(la_mere(julie)), F, A).
F = la_mere,
A = 1.
?- arg(1, la_mere(la_mere(julie)), A).
A = la_mere(julie).
Exemple d'emploi :
/* subst, repris de Sterling
&
Shapiro p. 140
subst(Old, New, Ancien, Moderne) ==
Moderne est Ancien dans lequel on a substitué
New à toutes les occurrences de Old
*/
subst(Old, New, Old, New). % le terme lui-même
subst(Old, New, Term, Term) :- atomic(Term), Term \= Old.
%the backslash (\)
is normally used to indicate negation in Prolog.
subst(Old, New, Term, Autre) :-
compound(Term),
functor(Term, F, N),
functor(Autre, F, N),
subst(N, Old, New, Term, Autre). % arité
4 !
subst(N, Old, New, Term, Autre) :-
N > 0,
arg(N, Term, ArgOld),
subst(Old, New, ArgOld, ArgNew),
arg(N, Autre, ArgNew),
M is N-1,
subst(M, Old, New, Term, Autre).
subst(0, Old, New, Terme, Autre).
Exécution :
?- subst(julie, marie, la_mere(la_mere(julie)), X).
X = la_mere(la_mere(marie)) ;
false.
?- subst(julie, marie, X, la_mere(la_mere(marie))).
false.
?- subst(julie, X, la_mere(la_mere(julie)), la_mere(la_mere(marie))).
X = marie ;
false.
?- subst(X, Y, la_mere(la_mere(julie)), la_mere(la_mere(marie))).
X = la_mere(la_mere(julie)),
Y = la_mere(la_mere(marie)) ;
X = la_mere(julie),
Y = la_mere(marie) ;
X = julie,
Y = marie ;
false.
-
Terme =.. [Fonc, Arg1, Arg2,...]
?- X =..[pere, max, toto].
X = pere(max, toto).
Exemple de mise en œuvre dans la section suivante.
-
assert(Fait) :
Ex: assert(pere(max, toto)).
?- assert(pere(max, toto)).
ERROR: assert/1: No permission to modify static_procedure `pere/2'
N'est possible (en SWI-Prolog) que si le prédicat binaire pere a
été déclaré dynamic
à la compilation : ":- dynamic pere/2." doit
figurer dans le fichier source.
assert(Clause) : assert((Tete :- Corps))
Attention au double parenthésage !
?- assert(
| (oncle_pat(X,Y) :-
| pere(U, Y), frere(U, X)
| )).
true.
avec deux variantes asserta (ajoute en
tête du paquet de clauses) et assertz
(id. en queue).
-
Même syntaxe.
son allié retractall pour prédicats
dynamiques : si pere avait été déclaré dynamic : retractall(pere(X,
Y)).
à rapprocher de abolish pour prédicats
statiques : dans le cas contraire abolish(pere/2).
-
Exemple : Un petit lecteur-évaluateur
interactif
d'exp.
arithmétiques
:- dynamic base/2.
go :- retractall(base(X, Y)), % DPFTR
encore.
encore :- nl, write('Lecture : '), read(Lu), traite(Lu).
traite($) :- !, write('Au-revoir'), nl.
traite(Exp) :- eval(Exp, Val), nl, write('Valeur de '), write(Exp),
write(' =
'), write(Val), nl, encore.
eval(Exp, Exp) :- number(Exp), !.
eval(Exp, Val) :- atomic(Exp), !, valbase(Exp, Val).
eval(Exp, Val) :- functor(Exp, F, 2),
arg(1,
Exp, Ag), arg(2,Exp,Ad),
eval(Ag, Valg), eval(Ad, Vald),
T =..[F, Valg, Vald], Val is T.
valbase(Var, Val) :- base(Var, Val), !.
valbase(Var, Val) :- nl, write('Valeur de '), write(Var), write(' ? '),
read(Val), assert(base(Var, Val)). % une
seule valeur par "variable"
Exécution :
?- go.
Lecture : x+y-2*x.
Valeur de x ? 3.
Valeur de y ? 4.
Valeur de x+y-2*x = 1
Lecture : x+y+z.
Valeur de z ? 3.
Valeur de x+y+z = 10
Lecture : '$'.
Au-revoir
true.
-
Autre exemple de l'emploi d'assert/retract
: AZERTYOP.
Exemple de conversation :
?- azer.
À vos ordres M'sieu !
|: montre.
1 est par terre
2 est par terre
3 est par terre
4 est sur 1
Et voila tout !
À vos ordres M'sieu !
|: pose(4,4).
Ça s'peut pas M'sieu !
À vos ordres M'sieu !
|: pose(4,1).
Il y est déjà M'sieu !
À vos ordres M'sieu !
|: poser(1,4).
J'compran pas M'sieu !
poser(1, 4)
À vos ordres M'sieu !
|: pose(1,4).
J'ai posé 4 par terre
J'ai posé 1 sur 4
À vos ordres M'sieu !
|: pose(9,10).
9 n'est pas un cube !
10 n'est pas un cube !
Y m'faut des cubes M'sieu !
À vos ordres M'sieu !
|: pose(3,1).
J'ai posé 3 sur 1
À vos ordres M'sieu !
|: montre.
2 est par terre
4 est par terre
1 est sur 4
3 est sur 1
Et voila tout !
À vos ordres M'sieu !
|: pose(4,2).
J'ai posé 3 par terre
J'ai posé 1 par terre
J'ai posé 4 sur 2
À vos ordres M'sieu !
|: fin.
Au revoir
false.
Le programme
/****************************************************************************/
/*
A Z E R T Y O P de P. Greussay,
adapté à Prolog par J-F. Perrot
*/
/******************************************************************************/
/* Utilitaires
printlist([]):- nl.
printlist([T|C]):- write(T),printlist(C).
*/
printlist(L) :- maplist(write, L), nl.
/* L'univers d'AZERTYOP */
cube(0).
cube(1).
cube(2).
cube(3).
cube(4).
:- dynamic sur/2.
init :-
retractall(sur(X, Y)),
assert(sur(1,0)),
assert(sur(4,1)),
assert(sur(2,0)),
assert(sur(3,0)).
/* D'abord une boucle infinie d'interaction
"toplevel"
*/
azer :- init, encore.
encore :-
nl,
printlist(['À vos ordres M\'sieu ! ']), nl,
read(C), exec(C),
encore.
/*
Les tâches
d'AZERTYOP
*/
exec(fin):- !,printlist(['Au ', revoir]), fail.
exec(montre):- !, montre.
exec(pose(X,Y)):- verifie(X,Y), !, pose(X,Y).
exec(pose(X,Y)):- !, printlist(['Y m\'faut des cubes M\'sieu ! ']).
exec(X):- printlist(['J\'compran pas M\'sieu ! ']),
tab(15), write(X), nl.
montre:- sur(X,0), write(X), write(' est par terre'), nl, fail.
montre:- sur(X,Y), Y \= 0, write(X), write(' est sur '), write(Y),
nl, fail.
montre:- printlist([' Et voila tout !']), nl.
pose(0,X):- !, printlist(['J\'peux pas poser la terre M\'sieu !']), nl.
pose(X,X):- !, printlist(['Ça s\'peut pas M\'sieu !']), nl.
pose(X,Y):- sur(X,Y), !, printlist(['Il y est déjà M\'sieu !']), nl.
pose(X,Y):- degager(X), degager(Y),
retract(sur(X,_)), !, /* pas de
back-track sur
"retract" */
assert(sur(X,Y)), chante(X,Y).
chante(X,0) :- !, write('J\'ai posé '), write(X), write(' par terre'),
nl.
chante(X,Y) :- write('J\'ai posé '), write(X), write(' sur '),
write(Y), nl.
degager(0):- !.
degager(X):- sur(Y,X), !, pose(Y,0).
degager(X).
verifie(X,Y):- cube(X), !, verif2(Y).
verifie(X,Y):- printlist([X, ' n\'est pas un cube !']), verif2(Y), fail.
verif2(Y) :- cube(Y), !.
verif2(Y) :- printlist([Y, ' n\'est pas un cube !']), fail.
-
l'ensemble étant représenté par une liste ordonnée (ordre standard des
termes) sans répétition.
Les variables du terme FormeInstance ne
doivent pas réapparaître ailleurs que dans le LittéralPrédicat.
Elles sont liées dans le setof.
Exemple (avec la seconde famille) :
?- setof(X, pere(cesar, X), S).
S = [adrienne, marc].
?- setof(mere(X), pere(cesar, X), S).
S = [mere(adrienne), mere(marc)].
Backtrack sur variable libre
dans LittéralPrédicat
:
?- setof(Y, pere(Y, X), S).
X = adrienne,
S = [cesar] ;
X = antoine,
S = [marc] ;
X = cesar,
etc.
-
La normalisation de la liste des résultats opérée par
setof
coûte cher en temps de calcul.
Le prédicat bagof fait la même chose sans
normaliser,
donc avec les éventuelles répétitions et suivant l'ordre de la
démonstration.
Il répond donc exactement au besoin de manipuler par programme la liste
complète des résultats.
Exemple :
/* Enumeration des chemins d'un
graphe sans
circuit */
/* Le graphe est donne' par le predicat "arc", ses sommets sont des
atomes */
chemin(0, Org, [Org]). /* "Org" comme "origine" */
chemin(R, Org, [Org|S]):- arc(Org, Next), RN is R-1,
chemin(RN, Next, S).
lesChemins(R, Org, Liste) :- bagof(Ch, chemin(R, Org, Ch), Liste).
showChemins(R, Org) :- lesChemins(R, Org, Liste), lwrite(Liste).
lwrite([]) :- write('Et voila tout !').
lwrite([Ch|S]) :- write(Ch), nl, lwrite(S).
% mieux que maplist(write, Liste)
/* Premiere generation */
/* Le couple (a1, b1) a trois enfants a2, b2, c2 */
arc(a1, a2). arc(b1, a2). arc(a1, b2). arc(b1, b2).
arc(a1, c2). arc(b1, c2).
/* Le couple (x1, y1) en a deux x2, y2 */
arc(x1, x2). arc(y1, x2). arc(x1, y2). arc(y1, y2).
/* Le couple (u1, v1) en a deux u2, v2 */
arc(u1, u2). arc(v1, u2). arc(u1, v2). arc(v1, v2).
/* Le couple (z1, t1) en a un t2 */
arc(z1, t2). arc(t1, t2).
/* Deuxieme generation */
/* a2 avec y2 engendrent x3 et y3 */
arc(a2, x3). arc(y2, x3). arc(a2, y3). arc(y2, y3).
/* b2 avec v2 engendrent u3 et v3 */
arc(b2, u3). arc(v2, u3). arc(b2, v3). arc(v2, v3).
/* x2 avec c2 engendrent c3 et t3 */
arc(x2, c3). arc(c2, c3). arc(x2, t3). arc(c2, t3).
/* u2 avec t2 engendrent a3 et b3 */
arc(u2, a3). arc(t2, a3). arc(u2, b3). arc(u2, b3).
/* Troisieme generation */
/* a3 avec y3 engendrent x4 et y4 */
arc(a3, x4). arc(y3, x4). arc(a3, y4). arc(y3, y4).
/* b3 avec v3 engendrent u4 et v4 */
arc(b3, u4). arc(v3, u4). arc(b3, v4). arc(v3, v4).
/* x3 avec c3 engendrent c4 et t4 */
arc(x3, c4). arc(c3, c4). arc(x3, t4). arc(c3, t4).
/* u3 avec t3 engendrent a4 et b4 */
arc(u3, a4). arc(t3, a4). arc(u3, b4). arc(u3, b4).
/* Quatrieme generation */
/* a4 avec y4 engendrent x5 et y5 */
arc(a4, x5). arc(y4, x5). arc(a4, y5). arc(y4, y5).
/* b4 avec v4 engendrent u5 et v5 */
arc(b4, u5). arc(v4, u5). arc(b4, v5). arc(v4, v5).
/* x4 avec c4 engendrent c5 et t5 */
arc(x4, c5). arc(c4, c5). arc(x4, t5). arc(c4, t5).
/* u4 avec t4 engendrent a5 et b5 */
arc(u4, a5). arc(t4, a5). arc(u4, b5). arc(u4, b5).
Exécution :
?- showChemins(3, x1).
[x1, x2, c3, c4]
[x1, x2, c3, t4]
[x1, x2, t3, a4]
[x1, y2, x3, c4]
[x1, y2, x3, t4]
[x1, y2, y3, x4]
[x1, y2, y3, y4]
Et voila tout !
true.
-
Le
LittéralPrédicat dans le setof
peut être composé par
- conjonction (notée par la virgule "
,"),
- disjonction (notée par le point-virgule "
;")
- quantification existentielle
Var^Terme
(comme opérateur extérieur)
Exemples :
?- setof(X, Y^pere(Y, X), S).
S = [adrienne, antoine, cesar, enza, lea, mara, marc, paul].
?- setof(X, Y^(pere(Y,X), masc(X)), S).
S = [cesar, marc].
mais pas setof(X, (Y^pere(Y,X), masc(X)), S) qui est
logiquement équivalent.
?- setof(X, Y^Z^(pere(Y,X), masc(X) ; mere(Z, X), fem(X)),
S).
S = [cesar, enza, lea, marc].
?- bagof(X, Y^(pere(Y, X) ; mere(X,
Y)), S).
S =
[cesar,lea,adrienne,enza,marc,mara,antoine,paul,silvia,julie,lea,pippa,lea,enza,enza].
Quid de la négation ??? Limitation de la négation par échec...
Le "minimum" setof(X, not(pere(jules, X)), S)
renvoie false
(dans des versions précédentes de Prolog, il provoquait une erreur !)
-
-
Les "faits" vrais ou faux dont on parle (variables propositionnelles)
sont censés se rapporter à un objet du discours
qui reste implicite : dans l'exemple qui suit, il s'agit d'un
quadrilatère dont on cherche à déterminer la nature.
Ces faits sont représentés par des atomes Prolog, p.ex. "carre"
ou "losange"
pour dire que le quadrilatère en question
est (ou n'est pas) un carré ou un
losange.
Les faits connus comme vrais (qui composent la "base de faits") sont
déterminés par le prédicat "fait",
p.ex. "fait(rectangle)."
-
Les règles expriment des relations logiques entre faits :
par exemple, si le quadrilatère en question est à la fois rectangle
et losange, alors il est carré.
Format des règles : clauses de Horn propositionnelles
[ conclusion | liste de
prémisses ],
connues via le prédicat "regle",
p.ex. "regle([carre, rectangle, losange])."
Exemple complet d'une base de règles ci-après.
-
Commentaires
- Dans ce genre de réalisations, l'idée est d'avoir
un moteur
d'inférences séparé de la base de règles.
La base de règles (alias base de connaissances) est censée
représenter le savoir d'un "expert",
exposé suivant sa logique propre, sans se préoccuper des contraintes
opérationnelles induites par le moteur.
Le présent exemple cherche à illustrer ce principe d'une manière
minimale : nos bases de règles sont exploitables
aussi bien par un moteur en marche arrière que par un moteur en marche
avant, comme on va le voir.
- La grande difficulté est de construire des bases de
règles
"intéressantes" : comme on s'en apercevra bien vite,
le cadre de "l'ordre 0 strict" est trop étroit pour y déployer des
connaissances substantielles.
La base des quadrilatères ci-après donne lieu à des raisonnements qui
illustrent bien le principe.
Mais je ne suis pas arrivé à construire d'autres bases de la même
"qualité" : à titre de comparaison,
en voici une autre à caractère zoologique - hélas beaucoup moins
intéressante sur le plan du raisonnement.
-
Prédicat
pprouver(But, EnAttente), le second
argument pour éviter de boucler,
et son itéré lprouver pour listes de buts
:- dynamic(fait/1).
:- dynamic(deduit/2).
prouver(But) :- pprouver(But, []).
pprouver(But, BEA) :- fait(But),!.
pprouver(But, BEA) :- membre(But, BEA), !, fail.
pprouver(But, BEA) :- regle([But | Premisses]),
lprouver(Premisses, [But|BEA]),
assert(fait(But)),
assert(deduit(But, Premisses)). /* pour les explications */
lprouver([], BEA).
lprouver([P|S], BEA) :- pprouver(P, BEA), lprouver(S, BEA).
membre(X, [X|S]) :- !.
membre(X, [_|S]) :- membre(X, S).
-
saturer :- nouveau(_),!,
saturer.
saturer :- write('Saturation terminee'), nl.
nouveau(Z) :- regle([Z|Prem]), not(fait(Z)), lfait(Prem),
assert(fait(Z)), /* essentiel ! */
assert(deduit(Z, Prem)). /* pour les
explications */
lfait([]).
lfait([X | R]) :- fait(X), lfait(R).
-
:- dynamic(deja_vu/1).
pourquoi(Fait) :- explique(Fait, 0).
explique(Fait, Prof) :- deja_vu(Fait), !, tab(Prof),
write('Le
fait "'), write(Fait),
write('"
a ete obtenu precedemment.'), nl.
explique(Fait, Prof) :- deduit(Fait, LPrem), !, tab(Prof),
write('J''ai deduit "'), write(Fait), write('" de '),
write(LPrem), nl, Profp is Prof+1,
lexplique(LPrem, Profp),
tab(Prof),
write('Ceci acheve la preuve de "'), write(Fait),
write('"'), nl, assert(deja_vu(Fait)).
explique(Fait, Prof) :- fait(Fait), !, tab(Prof),
write('Le
fait "'), write(Fait),
write('"
fait partie des hypotheses initiales.'), nl.
explique(Fait, Prof) :-
write('Mais j''ai jamais pretendu que "'), write(Fait),
write('"
!'), nl.
lexplique([], _).
lexplique([Fait|SFaits], Prof) :- explique(Fait, Prof),
lexplique(SFaits, Prof).
-
/* (1) Formulation
explicite des
proprietes evoquees */
/* Le vocabulaire et sa signification : on rappelle que le discours se
refere a un quadrilatere hypothetique dont il s'agit de determiner la
nature et les proprietes */
trad(carre, 'Le quadrilatere est un carre').
trad(losange, 'Le quadrilatere est un losange').
trad(rectangle, 'Le quadrilatere est un rectangle').
trad(parallelogramme, 'Le quadrilatere est un
parallelogramme').
trad(trapeze, 'Le quadrilatere est un trapeze').
trad(trapeze_isocele, 'Le quadrilatere est un trapeze
isocele').
trad(trapeze_rectangle, 'Le quadrilatere est un trapeze
rectangle').
trad(inscriptible, 'Le quadrilatere est inscriptible (dans un
cercle)').
trad(diag_egales, 'Les diagonales sont egales').
trad(diag_ortho, 'Les diagonales sont orthogonales').
trad(diag_milieu, 'Les diagonales se coupent en leur milieu').
trad(ang_op_suppl, 'Les angles opposes sont supplementaires').
trad(ang_op_egaux, 'Les angles opposes sont egaux').
trad(deux_ang_op_droits, 'Il y a deux angles droits opposes ').
trad(quatre_ang_droits, 'Les quatre angles sont droits').
trad(un_ang_droit, 'Il y a un angle droit').
trad(quatre_cotes_egaux, 'Les quatre cotes sont egaux').
trad(cotes_op_egaux, 'Les cotes opposes sont egaux').
trad(cotes_op_paralleli, 'Les cotes opposes sont paralleles').
trad(deux_cotes_op_egaux, 'Il y a deux cotes opposes egaux').
trad(deux_cotes_op_par, 'Il y a deux cotes opposes paralleles').
trad(deux_cotes_adj_egaux, 'Il y a deux cotes adjacents egaux').
/* Application a l'explicitation des regles, dont le format est celui
de clauses de Horn propositionnelles [Concusion | Premisses].
Exemple : pour la regle "[carre, rectangle, losange]" on developpera :
SI Le quadrilatere est un rectangle
ET SI Le quadrilatere est un losange
ALORS Le quadrilatere est un
carre */
tradregle([Concl, Prem1|SPrem]) :- write('SI '),
trad(Prem1, T), write(T), nl, tradprem(SPrem),
write('ALORS '), tradconcl(Concl).
tradprem([]).
tradprem([P|S]) :- write('ET SI '), trad(P, T), write(T), nl,
tradprem(S).
tradconcl(C) :- trad(C, T), write(T), nl.
/* (2) LISTE DES REGLES, par centres d'interet */
/* Carres et losanges */
regle([carre, rectangle, losange]).
regle([rectangle, carre]).
regle([losange, carre]).
regle([carre, inscriptible, diag_ortho]).
regle([parallelogramme, losange]).
regle([losange, parallelogramme, diag_ortho]).
regle([losange, parallelogramme, deux_cotes_adj_egaux]).
regle([losange, quatre_cotes_egaux]).
regle([quatre_cotes_egaux, losange]).
/* Rectangles */
regle([rectangle, quatre_ang_droits]).
regle([quatre_ang_droits, rectangle]).
regle([parallelogramme, rectangle]).
regle([rectangle, parallelogramme, un_ang_droit]).
regle([un_ang_droit, rectangle]).
regle([rectangle, parallelogramme, inscriptible]).
regle([inscriptible, rectangle]).
regle([rectangle, parallelogramme, diag_egales]).
regle([diag_egales, rectangle]).
/* Parallelogrammes */
regle([parallelogramme, cotes_op_egaux]).
regle([cotes_op_egaux, parallelogramme]).
regle([parallelogramme, cotes_op_par]).
regle([cotes_op_par, parallelogramme]).
regle([parallelogramme, diag_milieu]).
regle([diag_milieu, parallelogramme]).
regle([parallelogramme, ang_op_egaux]).
regle([ang_op_egaux, parallelogramme]).
/* Trapezes */
regle([trapeze, deux_cotes_par]).
regle([deux_cotes_par, trapeze]).
regle([trapeze_rectangle, trapeze, un_ang_droit]).
regle([trapeze, trapeze_rectangle]).
regle([un_ang_droit, trapeze_rectangle]).
regle([trapeze, trapeze_isocele]). /* deux cotes op egaux mais pas un
parallelogramme */
regle([trapeze_isocele, trapeze, diag_egales]).
regle([diag_egales, trapeze_isocele]).
regle([trapeze_isocele, trapeze, inscriptible]).
regle([inscriptible, trapeze_isocele]).
regle([deux_cotes_op_egaux, trapeze_isocele]).
/* Regles "generales" */
regle([un_ang_droit, quatre_ang_droits]).
regle([deux_ang_op_droits, quatre_ang_droits]).
regle([deux_ang_op_droits, un_ang_droit, ang_op_suppl]).
regle([deux_ang_op_droits, un_ang_droit, ang_op_egaux]).
regle([quatre_ang_droits, ang_op_suppl, ang_op_egaux]).
regle([deux_ang_op_egaux, ang_op_egaux]).
regle([deux_ang_op_egaux, deux_ang_op_droits]).
regle([inscriptible, ang_op_suppl]).
regle([ang_op_suppl, inscriptible]).
regle([deux_cotes_par, cotes_op_par]).
regle([cotes_op_par, deux_cotes_par, deux_ang_op_egaux]).
regle([cotes_op_egaux, quatre_cotes_egaux]).
regle([deux_cotes_adj_egaux, quatre_cotes_egaux]).
regle([deux_cotes_op_egaux, quatre_cotes_egaux]).
regle([quatre_cotes_egaux, cotes_op_egaux, deux_cotes_adj_egaux]).
-
?- assert(fait(trapeze_rectangle)).
true.
?- assert(fait(trapeze_isocele)).
true.
?- prouver(rectangle). % en marche arrière
true .
?- pourquoi(rectangle).
J'ai deduit "rectangle" de [quatre_ang_droits]
J'ai deduit "quatre_ang_droits" de [ang_op_suppl,
ang_op_egaux]
J'ai deduit "ang_op_suppl" de [inscriptible]
J'ai deduit "inscriptible" de [trapeze_isocele]
Le fait "trapeze_isocele" fait partie
des hypotheses initiales.
Ceci acheve la preuve de "inscriptible"
Ceci acheve la preuve de "ang_op_suppl"
J'ai deduit "ang_op_egaux" de [parallelogramme]
J'ai deduit "parallelogramme" de [cotes_op_par]
J'ai deduit "cotes_op_par" de
[deux_cotes_par, deux_ang_op_egaux]
J'ai deduit "deux_cotes_par"
de [trapeze]
J'ai deduit
"trapeze" de [trapeze_rectangle]
Le fait
"trapeze_rectangle" fait partie des hypotheses initiales.
Ceci acheve la
preuve de "trapeze"
Ceci acheve la preuve de
"deux_cotes_par"
J'ai deduit
"deux_ang_op_egaux" de [deux_ang_op_droits]
J'ai deduit
"deux_ang_op_droits" de [un_ang_droit, ang_op_suppl]
J'ai
deduit "un_ang_droit" de [trapeze_rectangle]
Le fait "trapeze_rectangle" fait partie des hypotheses initiales.
Ceci
acheve la preuve de "un_ang_droit"
Le fait
"ang_op_suppl" a ete obtenu precedemment.
Ceci acheve la
preuve de "deux_ang_op_droits"
Ceci acheve la preuve de
"deux_ang_op_egaux"
Ceci acheve la preuve de "cotes_op_par"
Ceci acheve la preuve de "parallelogramme"
Ceci acheve la preuve de "ang_op_egaux"
Ceci acheve la preuve de "quatre_ang_droits"
Ceci acheve la preuve de "rectangle"
true.
?- fait(X), writeln(X), fail. % la
collection des faits établis au cours de la preuve
trapeze_rectangle
% dans l'ordre chronologique de leur
démonstration
trapeze_isocele
inscriptible
ang_op_suppl
inscriptible
trapeze
deux_cotes_par
un_ang_droit
deux_ang_op_droits
deux_ang_op_egaux
cotes_op_par
parallelogramme
ang_op_egaux
quatre_ang_droits
rectangle
% comme il est normal, c'est le dernier à avoir
été établi
false.
?- saturer. % en marche avant
Saturation terminee
true.
?- fait(X), writeln(X), fail.
trapeze_rectangle
trapeze_isocele
inscriptible
ang_op_suppl
inscriptible
trapeze
deux_cotes_par
un_ang_droit
deux_ang_op_droits
deux_ang_op_egaux
cotes_op_par
parallelogramme
ang_op_egaux
quatre_ang_droits
rectangle
diag_egales % conséquences qui
n'avaient pas encore été prises en compte...
cotes_op_egaux
diag_milieu
deux_cotes_op_egaux
false.
?- pourquoi(deux_cotes_op_egaux).
J'ai deduit "deux_cotes_op_egaux" de [trapeze_isocele]
Le fait "trapeze_isocele" fait partie des hypotheses
initiales.
Ceci acheve la preuve de "deux_cotes_op_egaux"
true.
-
/* tous_diff(Liste)
<=> tous
les elements de la Liste sont differents
deux a deux */
tous_diff([]).
tous_diff([A|S]) :- not(member(A, S)), tous_diff(S).
/* Arithmetique */
chiffre(0). chiffre(1). chiffre(2). chiffre(3). chiffre(4).
chiffre(5). chiffre(6). chiffre(7). chiffre(8). chiffre(9).
col(Reste_p, Ch1, Ch2, Chr, Reste_n) :- chiffre(Ch1), chiffre(Ch2),
Somme is
Reste_p+Ch1+Ch2,
Reste_n
is Somme//10, Chr is Somme mod 10.
/* L'enonce : Generate & Test */
sol([S,E,N,D,M,O,R,Y]) :-
col( 0, D, E, Y, R1),
col(R1, N, R, E,
R2),
col(R2, E, O, N, R3),
col(R3, S, M, O, R4),
col(R4, 0, 0, M, 0),
not(M=0),
tous_diff([S,E,N,D,M,O,R,Y]).
/* La jolie impression */
joli([S,E,N,D,M,O,R,Y]) :- nl,
tab(10),
write(S), write(E), write(N), write(D), nl,
tab(7), write(' + '), write(M), write(O),
write(R), write(E), nl,
tab(8), write('------'), nl,
tab(9), write(M), write(O), write(N),
write(E), write(Y),
nl.
/* Le predicat d'appel */
ca :- sol([S,E,N,D,M,O,R,Y]), joli([S,E,N,D,M,O,R,Y]), fail.
Exécution
?- ca.
9567
+ 1085
------
10652
false.
-
Pour essayer les nombreux exemples qu'on trouve sur le réseau...
/* Le compilateur de problèmes
cryptarithmétiques */
:- dynamic(sol/1).
/* Auxiliaires */
rev(L, R) :- revl(L, [], R).
revl([], R, R).
revl([X|S], T, R) :- revl(S, [X|T], R).
concat([], X, X).
concat([A | B], C, [A | D]) :- concat(B, C, D).
/* member(X, [X|S]) :- !.
member(X, [Y|S]) :- member(X, S). */
/* pour l'exe'cution ... */
tous_diff([]).
tous_diff([A|S]) :- not(member(A, S)), tous_diff(S).
chiffre(0). chiffre(1). chiffre(2). chiffre(3). chiffre(4).
chiffre(5). chiffre(6). chiffre(7). chiffre(8). chiffre(9).
col(Reste_p, Ch1, Ch2, Chr, Reste_n) :- chiffre(Ch1), chiffre(Ch2),
Somme is
Reste_p+Ch1+Ch2,
Reste_n
is Somme//10, Chr is Somme mod 10.
/* Queue de la clause */
csq(U, V, W, C) :- rev(U, RU), rev(V, RV), rev(W, RW),
rcsq(RU, RV, RW, C).
rcsq([DU|SU], [DV|SV], [DW|SW], ((col(0, DU, DV, DW, R), CS))) :-
rcss(SU, SV, SW, R, CS).
rcss([], [], [PW], R, ((col(R, 0, 0, PW, 0), not(PW = 0)))). /* arret 1
*/
rcss([PU], [PV], [PW], R, ((col(R, PU, PV, PW, 0), not(PW = 0)))).
/*arret2*/
rcss([NU|SU], [NV|SV], [NW|SW], R, ((col(R, NU, NV, NW, RN), CS))) :-
rcss(SU, SV, SW, RN, CS). /* avec
creation d'une nouvelle var ds RN */
/* Le predicat-maitre */
csol(U, V, W, ((sol(LV) :- (Q, tous_diff(LV))))) :-
concat(U, V, UV), concat(UV, W, UVW),
sort(UVW, LV), csq(U, V, W, Q).
/* Auxiliaires pour la jolie impression */
long([], 0).
long([X|S], K) :- long(S, H), K is H+1.
ligne([]) :- nl.
ligne([X|S]) :- V is X, write(V), ligne(S).
trait(0):- !, nl.
trait(N) :- write('-'), M is N-1, trait(M).
/* La jolie impression */
ijoli(D, U, V, W) :- long(U, H), long(V, K), long(W, L),
iijoli(D, U, V, W, H, K, L).
iijoli(D, U, V, W, H, H, H) :- /* les trois de meme longueur
*/
nl, tab(D), tab(2),
ligne(U),
tab(D), write('+ '),
ligne(V),
tab(D), K is H+2,
trait(K),
tab(D), tab(2),
ligne(W).
iijoli(D, U, V, W, H, H, L) :- L is H+1, !, /* un de plus pour la somme
*/
nl, tab(D), tab(2),
ligne(U),
tab(D), write('+ '),
ligne(V),
tab(D), K is H+2,
trait(K),
tab(D), tab(1),
ligne(W).
iijoli(D, U, V, W, H, K, K) :- H < K, !, DH is K-H,
nl, tab(D), tab(2),
tab(DH), ligne(U),
tab(D), write('+ '),
ligne(V),
tab(D), T is K+2,
trait(T),
tab(D), tab(2),
ligne(W).
iijoli(D, U, V, W, H, K, H) :- K < H, !, DK is H-K,
nl, tab(D), tab(2),
ligne(U),
tab(D), write('+ '),
tab(DK), ligne(V),
tab(D), T is H+1,
trait(T),
tab(D), tab(1),
ligne(W).
/* Exe'cution avec jolie impression */
auvol(U, V, W) :- csol(U,V,W,(T :- Q)), assert((T :- Q)),
call(T), ijoli(15, U,V,W).
/* Essais */
av1 :- auvol([S,E,N,D], [M,O,R,E], [M,O,N,E,Y]).
av2 :- auvol([B,I,G], [B,O,Y], [M,A,N]).
av3 :- auvol([D,O,N,A,L,D], [G,E,R,A,L,D], [R,O,B,E,R,T]).
Exécution
?- av3.
526485
+ 197485
--------
723970
true ;
false.