Programmation Logique.docx

RAPPORT PROLOG SOMMAIRE Rappel du sujet Particularités du PROLOG Problème n°1 : Missionnaires et Cannibales Problème n°2 : Qui fait quoi ? Utilisation d’une pile RAPPEL DU SUJET La programmation PROLOG recèle un certain nombre de particularités. Vous en retiendrez 3, les exposerez, les expliquerez, en direz l’importance. Puis vous décrirez et programmerez des exemples pour les mettre en valeur. Le nombre d’exemples requis n’est pas fixé. La seule requête est que l’on puisse bien voir les 3 comportements que vous avez retenus, ce qu’ils apportent, comment cela fonctionne, etc. Un seul exemple bien choisi peut être parfait. Bien sûr, vous commenterez vos exemples, leurs exécutions sur des jeux de tests éventuellement, de manière à montrer qu’ils sont bien choisis. PARTICULARITES DU PROLOG Prolog(PROgrammation LOGique) est un langage utilisé en intelligence artificielle pour effectuer des raisonnements à partir d’une formalisation logique des problèmes. Il est utilisé dans des applications telles que la modélisation du dialogue homme/machine, la planification en robotique... Le cerveau d’un système Prolog est un moteur d’inférences associé à un formalisme d ‘écriture de règles qui effectue des raisonnements en chaînage arrière selon la logique du calcul des prédicats. Prolog consiste à écrire des relations entre les prédicats et à poser des problèmes en termes de buts à atteindre. L’ordre d‘écriture des clauses est important en Prolog. L’algorithme de résolution utilisé par Prolog met en œuvre une exploration en profondeur d’abord d’un arbre et autorise un retour en arrière. En cas d’échec (c’est à dire au cas où on ne pourrait plus appliquer aucune règle) revenir en arrière, au plus récent point de raisonnement où une règle pouvait être encore appliquée, est appelé backtracking. Le retour en arrière permet de gérer ces échecs et de trouver toutes les réfutations possibles. Il permet de trouver toutes les solutions possibles à un problème d’existence. Prolog cherche donc toutes les façons de satisfaire un but tant que celui-ci n’est pas atteint. L’autre particularité de Prolog est son non déterminisme. Le comportement d’un programme déterministe est totalement prévisible : chaque fonction retourne toujours la même valeur pour les mêmes arguments donnés en entrée. Une clause Prolog fonctionnera différemment selon le contexte dans lequel elle sera invoquée. C’est ce qui permet à Prolog de trouver plusieurs solutions différentes pour un problème donné. L’idée est de donner à l’ordinateur un ensemble d’hypothèses et de lui demander si l’on peut en déduire une conclusion en le faisant raisonner par résolution. En parcourant les cours de PROLOG il nous est apparu que le concept des piles est un concept fort, utilisé en permanence par PROLOG. C’est pourquoi nous avons choisi les piles en troisième particularité principale. Problème n°1 : Missionnaires et Cannibales Sujet: Trois missionnaires M et trois cannibales C se trouvent sur la même rive d’une rivière. Ils voudraient tous se rendre sur l’autre rive. Cependant, si le nombre de cannibales est supérieur à celui des missionnaires, alors les cannibales mangeront les missionnaires. Il faut donc que le nombre de missionnaires présents sur l’une ou l’autre des rives soit toujours supérieur à celui des cannibales. Le seul bateau disponible ne peut pas supporter le poids de plus de deux personnes. Comment est-ce que tout le monde peut traverser la rivière sans que les missionnaires risquent d’être mangé? Représentation du problème : Le schéma ci-dessous est un début des différentes possibilités envisageables pour trouver une solution à ce problème. Les cases barrées correspondent au cas impossibles qui ne satisfont pas la contrainte : nombre de missionnaires >= nombre de cannibales. 036195 00 381000177165C 00C 56896014414500 51054001905M 00M 4038600116205002133600116205MMMCCCB | 00MMMCCCB | 434340028575MM 00MM 129540028575C 00C 403860014287500152400014287500 44958001695450044196001695450026670005524500358140055245003810000552450024384005524500 274320081280CC 00CC 411480081280MCCC | BMM 00MCCC | BMM 83820081280MMMCC | BC 00MMMCC | BC 525780013462000525780013462000 175260046990CC 00CC 388620046990MC 00MC 472440046990MMCCC | BM 00MMCCC | BM 281940046990 MC 00 MC 3276600187960MMCC | BMC 00MMCC | BMC 1447800187960MMMC | BCC 00MMMC | BCC 441960012700000320040012700000114300012700000 487680038735M 00M 281940038735C 00C 76200038735C 00C 28194006540500289560065405004267200179705MMMCCB | C 00MMMCCB | C 2209800179705MMCCCB | M 00MMCCCB | M 304800179705MMMCCB | C 00MMMCCB | C Programme : %Prédicat d'appel solution(S):- etat_initial(Etat), chemin(Etat,[Etat],S),affichage(S). % Description des faits % Nous supposerons que ,au départ, les 3 missionnaires et les 3 cannibales se trouvent sur la rive gauche du fleuve % Nous noterons pour la suite m pour missionnaire, c pour cannibale, b pour bateau, g pour gauche et d pour droite etat_initial(etat(bg,cg(3),cd(0),mg(3),md(0))). etat_final(etat(bd,cg(0),cd(3),mg(0),md(3))). etat_legal(etat(bg,cg(CG),cd(CD),mg(MG),md(MD))):- CG==MG ; MD==0, CD>=MD. etat_legal(etat(bd,cg(CG),cd(CD),mg(MG),md(MD))):- MG==0, CG>=MG ; MD==0, CD>=MD. % Recherche d'un chemin chemin(Etat, _, []):- etat_final(Etat). chemin(Etat,Liste,[Voyager|S]):- voyage(Voyager, Etat, Nouveau), not(member(Nouveau,Liste)), chemin(Nouveau,[Nouveau|Liste],S). tete(X,[X|Xs],Xs). affichage([]). affichage(L):- tete(X,L,L1),write('\n'), write(X), affichage(L1). % Le bateau peut aussi bien naviguer de la rive gauche vers la rive droite que de la rive droite vers la rive gauche % Il y a 5 différents cas à considérer. On les notera de la manière suivante: % - 1M est le cas où 1 missionnaire prend le bateau % - 2M est le cas où 2 missionnaires prennent le bateau en même temps % - 1C est le cas où 1 cannibale prend le bateau % - 2C est le cas où 2 cannibales prennent le bateau en même temps % - 1M1C est le cas où 1 missionnaire et un cannibale prennent le bateau en même temps % Traitons d'abord tous les cas possibles pour aller de la rive gauche vers la rive droite voyage('1M traverse vers la rive droite', etat(bg,cg(CG),cd(CD),mg(MG),md(MD)), etat(bd,cg(CG),cd(CD),mg(MG1),md(MD1))):- MG>=1, MG1 is MG -1, MD1 is MD+1,etat_legal(etat(bd,cg(CG),cd(CD),mg(MG1),md(MD1))). voyage('2M traversent vers la rive droite', etat(bg,cg(CG),cd(CD),mg(MG),md(MD)), etat(bd,cg(CG),cd(CD),mg(MG1),md(MD1))):- MG>=2, MG1 is MG -2, MD1 is MD+2,etat_legal(etat(bd,cg(CG),cd(CD),mg(MG1),md(MD1))). voyage('1C traverse vers la rive droite', etat(bg,cg(CG),cd(CD),mg(MG),md(MD)), etat(bd,cg(CG1),cd(CD1),mg(MG),md(MD))):- CG>=1, CG1 is CG -1, CD1 is CD+1,etat_legal(etat(bd,cg(CG1),cd(CD1),mg(MG),md(MD))). voyage('2C traversent vers la rive droite', etat(bg,cg(CG),cd(CD),mg(MG),md(MD)), etat(bd,cg(CG1),cd(CD1),mg(MG),md(MD))):- CG>=2, CG1 is CG -2, CD1 is CD+2,etat_legal(etat(bd,cg(CG1),cd(CD1),mg(MG),md(MD))). voyage('1C et 1M traversent vers la rive droite', etat(bg,cg(CG),cd(CD),mg(MG),md(MD)), etat(bd,cg(CG1),cd(CD1),mg(MG1),md(MD1))):- MG>=1, CG>=1, MG1 is MG-1, CG1 is CG -1, MD1 is MD +1,CD1 is CD+1, etat_legal(etat(bd,cg(CG1),cd(CD1),mg(MG1),md(MD1))). % Cas possibles pour aller de la rive droite vers la rive gauche voyage('1M revient vers la rive gauche', etat(bd,cg(CG),cd(CD),mg(MG),md(MD)), etat(bg,cg(CG),cd(CD),mg(MG1),md(MD1))):- MD>=1, MD1 is MD -1, MG1 is MG+1,etat_legal(etat(bg,cg(CG),cd(CD),mg(MG1),md(MD1))). voyage('2M reviennent vers la rive gauche', etat(bd,cg(CG),cd(CD),mg(MG),md(MD)), etat(bg,cg(CG),cd(CD),mg(MG1),md(MD1))):- MD>=2, MD1 is MD -2, MG1 is MG+2,etat_legal(etat(bg,cg(CG),cd(CD),mg(MG1),md(MD1))). voyage('1C revient vers la rive gauche', etat(bd,cg(CG),cd(CD),mg(MG),md(MD)), etat(bg,cg(CG1),cd(CD1),mg(MG),md(MD))):- CD>=1, CD1 is CD -1, CG1 is CG+1,etat_legal(etat(bg,cg(CG1),cd(CD1),mg(MG),md(MD))). voyage('2C reviennent vers la rive gauche', etat(bd,cg(CG),cd(CD),mg(MG),md(MD)), etat(bg,cg(CG1),cd(CD1),mg(MG),md(MD))):- CD>=2, CD1 is CD-2, CG1 is CG+2,etat_legal(etat(bg,cg(CG1),cd(CD1),mg(MG),md(MD))). voyage('1C et 1M reviennent vers la rive gauche', etat(bd,cg(CG),cd(CD),mg(MG),md(MD)), etat(bg,cg(CG1),cd(CD1),mg(MG1),md(MD1))):- MD>=1, CD>=1, MD1 is MD-1, CD1 is CD -1, MG1 is MG +1,CG1 is CG+1, etat_legal(etat(bg,cg(CG1),cd(CD1),mg(MG1),md(MD1))). Solution : ?- solution(S). 2C traversent vers la rive droite 1C revient vers la rive gauche 2C traversent vers la rive droite 1C revient vers la rive gauche 2M traversent vers la rive droite 1C et 1M reviennent vers la rive gauche 2M traversent vers la rive droite 1C revient vers la rive gauche 2C traversent vers la rive droite 1M revient vers la rive gauche 1C et 1M traversent vers la rive droite S = ['2C traversent vers la rive droite', '1C revient vers la rive gauche', '2C traversent vers la rive droite', '1C revient vers la rive gauche', '2M traversent vers la rive droite', '1C et 1M reviennent vers la rive gauche', '2M traversent vers la rive droite', '1C revient vers la rive gauche', '2C traversent vers la rive droite'|...] ; 2C traversent vers la rive droite 1C revient vers la rive gauche 2C traversent vers la rive droite 1C revient vers la rive gauche 2M traversent vers la rive droite 1C et 1M reviennent vers la rive gauche 2M traversent vers la rive droite 1C revient vers la rive gauche 2C traversent vers la rive droite 1C revient vers la rive gauche 2C traversent vers la rive droite S = ['2C traversent vers la rive droite', '1C revient vers la rive gauche', '2C traversent vers la rive droite', '1C revient vers la rive gauche', '2M traversent vers la rive droite', '1C et 1M reviennent vers la rive gauche', '2M traversent vers la rive droite', '1C revient vers la rive gauche', '2C traversent vers la rive droite'|...] ; 1C et 1M traversent vers la rive droite 1M revient vers la rive gauche 2C traversent vers la rive droite 1C revient vers la rive gauche 2M traversent vers la rive droite 1C et 1M reviennent vers la rive gauche 2M traversent vers la rive droite 1C revient vers la rive gauche 2C traversent vers la rive droite 1M revient vers la rive gauche 1C et 1M traversent vers la rive droite S = ['1C et 1M traversent vers la rive droite', '1M revient vers la rive gauche', '2C traversent vers la rive droite', '1C revient vers la rive gauche', '2M traversent vers la rive droite', '1C et 1M reviennent vers la rive gauche', '2M traversent vers la rive droite', '1C revient vers la rive gauche', '2C traversent vers la rive droite'|...] ; 1C et 1M traversent vers la rive droite 1M revient vers la rive gauche 2C traversent vers la rive droite 1C revient vers la rive gauche 2M traversent vers la rive droite 1C et 1M reviennent vers la rive gauche 2M traversent vers la rive droite 1C revient vers la rive gauche 2C traversent vers la rive droite 1C revient vers la rive gauche 2C traversent vers la rive droite S = ['1C et 1M traversent vers la rive droite', '1M revient vers la rive gauche', '2C traversent vers la rive droite', '1C revient vers la rive gauche', '2M traversent vers la rive droite', '1C et 1M reviennent vers la rive gauche', '2M traversent vers la rive droite', '1C revient vers la rive gauche', '2C traversent vers la rive droite'|...] ; Commentaires : Le problème ci-dessus illustre parfaitement la notion de non déterminisme. En effet, pour les mêmes données (3 missionnaires et 3 cannibales), nous nous apercevons que en Prolog il existe 4 solutions bien distinctes. Nous avons donc trouver 4 différents parcours qui permettent de faire traverser tout le monde de l’autre côté de la rivière tout en respectant notre contrainte de départ. Lors de la recherche de solutions, le programme est revenu en arrière à chaque fois que cette contrainte n’était pas respectée. En effet, nous savons que l’ordre d’écriture des clauses est important en Prolog. Donc une première solution, s’il elle existe ,aurait du commencer par ‘1M traverse vers la rive droite’. Mais après avoir testé tous les parcours possibles à partir de la clause qui donne ce résultat, le programme revient en arrière (backtracking) et passe à la clause suivante jusqu’à arriver à la première clause permettant de réaliser un parcours qui donne ‘2C traversent vers la rive droite’. Les deux premières solutions sont sensiblement équivalentes. Et la encore l’ordre d’écriture des clauses dans le programme, implique un certain ordre lors de l’affichage des solutions. En effet, si on inversait dans le programme les deux clauses qui donnent ‘1M revient vers la rive gauche’ et 1C revient vers la rive gauche les solutions 1 et 2 seraient également inverser lors de l’affichage des solutions. A travers ce programme, nous avons pu étudier et illustrer 3 grandes particularités du Prolog qui sont : le non déterminisme, le chaînage arrière et l’ordre d’écriture des clauses. Problème n°2 : Qui fait quoi ? Sujet : Cette année, l'hypermarché Jumbo a accueilli en stage cinq élèves (Benoît, Françoise, Lydie, Sébastien, Stéphanie) des collèges voisins (Brassens, Diderot, Galois, Rabelais, Rostand). Retrouvez le prénom de chacun, le nom du collège, la durée du stage (de 1 à 5 semaines) et le rayon où chacun a été affecté (boucherie, fruits et légumes, ménage, saisonnier, vêtements). Propositions: 1. Françoise, qui est élève au collège Brassens, n'a pas travaillé au rayon ménage; Son stage a duré plus d'une semaine. 2. Benoît, qui n'est pas du collège Diderot, a effectué le plus long stage; Il n'a été affecté ni au rayon fruit et légumes ni au rayon ménage. 3. L’élève de Galois, qui n'est ni Benoît ni Stéphanie, a effectué un stage au rayon boucherie d'une durée supérieure à 2 semaines. 4. Au rayon vêtements Lydie est restée 2 semaines de plus que l'élève du collège Rabelais. Représentation du problème : Nous avons vu que Prolog est un langage qui raisonne. Comparons donc notre façon de penser à la sienne. Dans un programme en C, on impose notre façon de voir le problème, ce n’est pas forcément le cas pour Prolog. En effet, suivant la manière dont on lui pose un problème, Prolog va trouver ou non sa solution. C’est donc à nous de s’adapter à la logique Prolog. Modélisons le problème à travers un tableau : NOM ECOLE DUREE DU STAGE RAYON Benoît \=diderot \=galois 5 semaines \=fruits et\=ménage et \=boucherie Françoise Brassens >1 semaine \=ménage Lydie   durée rabelais+2 vêtement Sébastien       Stéphanie \=galois   \=boucherie A partir de ce tableau, en résonnant par élimination on peut facilement déterminer la solution de ce problème. Voyons maintenant comment s’y prend Prolog. Programme : % Prédicat d’appel solution(S):- S=[p(benoît,C1,R1,D1),p(francoise,C2,R2,D2),p(lydie,C3,R3,D3),p(sebastien,C4,R4,D4),p(stephane,C5,R5,D5)], % On rentre les hypothèses concernant les écoles : element_member([C1,C2,C3,C4,C5],[brassens,diderot,galois,rabelais,rostand]), all_different([C1,C2,C3,C4,C5]), C2==brassens, C1\==diderot, C1\==galois,=C5\==galois, % On rentre les hypothèses concernant les rayons : element_member([R1,R2,R3,R4,R5],[boucherie,fruit,menage,vetements,saisonnier]), all_different([R1,R2,R3,R4,R5]), R2\==menage, R1\==fruit, R1\==menage, R3==vetements, member(p(_,galois,boucherie,_),S), % On rentre les hypothèses concernant les durées : element_member([D1,D2,D3,D4,D5],[1,2,3,4,5]), all_different([D1,D2,D3,D4,D5]), D2\==1,D1==5, % On retire des solutions possibles les hypothèses que l’on sait fausses : not(member(p(_,galois,_,1),S)), not(member(p(_,galois,_,2),S)), %On rente l’hypothèse 4, celle-ci ne peut pas être exprimé directement, car elle se déduit d’autres hypothèses, on le dit à Prolog... member(p(_,rabelais,_,Dureerabelais),S), member(p(lydie,_,_,Dureelydie),S), Dureelydie is Dureerabelais+2. % fonction pour éviter les répétition dans les propositions, notion d’intégrité (par exemple, une seule personne peut s’appeler benoît). /* all_different/1 */ all_different([L1|L2]):-all_different(L2),not(member(L1,L2)). all_different([_]). all_different([]). % fonction d’appartenance ou de non appartenance à l’ensemble des solutions: /* element_member/2 */ element_member([X|Y],L2):-element_member(Y,L2),member(X,L2). element_member([],[]). element_member(X,X). element_member([X],L2):-member(X,L2). Après exécution, le programme nous donne le résultat suivant, qui est unique: 1 ?- solution(S). S = [p(benoit, rostand, saisonnier, 5), p(francoise, brassens, fruit, 2), p(lydie, diderot, vetements, 3), p(sebastien, galois, boucherie, 4), p(stephane, rabelais, menage, 1)] Comment le programme a-t-il raisonné pour arriver à cette conclusion ? On sait que le terme solution(S) est une règle qui ne se réalisera que si toutes les conditions énoncées dans son corps sont accomplies, c'est-à-dire que l’on satisfasse à toutes les hypothèses. Prolog va donc aller vérifier les hypothèses une à une pour trouver la solution. Si il tombe sur une erreur dans son raisonnement, il va revenir en arrière, c’est le backtraking, déjà vu plus haut. Le principe est simple. Prolog traduit les problèmes en arbre, dont les nœuds sont formés des différentes hypothèses données dans le programme. Prolog va parcourir l’arbre jusqu’à tomber sur une hypothèse non vérifié, il va la considérer comme fausse, et remonter au nœud précédent pour suivre un autre chemin, ainsi de suite jusqu’à trouver le résultat. Cela lui permet de raisonner par élimination (un peu comme nous) mais à la différence de nous, Prolog ne peut pas voir l’ensemble des hypothèses et trouver la solution par déduction. Il va passer en revu tout les cas pour les éliminer un à un. Celui qui restera sera forcément le bon. C’est très visible avec ce problème qui ne peut avoir qu’une seule et unique solution. Une autre particularité du Prolog que ce problème utilise est celle des listes. Une liste est une suite ordonnée d’éléments entre crochets, séparés par des virgules. Ici, tout le problème est traité par l’utilisation de liste. Par exemple, les différents rayons auxquels les stagiaires ont éventuellement pu faire leur stage sont implémentés sous forme de liste. element_member([R1,R2,R3,R4,R5],[boucherie,fruit,menage,vetements,saisonnier]), Un exemple remarquable de l’utilisation des listes dans le programme est la fonction all_diferent/1. /* all_different/1 */ all_different([L1|L2]):-all_different(L2),not(member(L1,L2)). all_different ([_]). all_different([]). En effet, celle-ci va prendre la tête (premier élément) et la queue (les autres éléments) de la liste, et va comparer la tête à tous les autres éléments de la liste pour vérifier qu’elle n’y est pas en double. Puis elle va prendre la queue de la liste et faire de même, ainsi de suite jusqu’à vérification de tous les éléments de la liste. C’est l’une des applications des listes. Ainsi, au travers de ce deuxième exemple, nous avons pu illustrer deux particularités du Prolog : le backtraking et l’utilisation des listes. Utilisation d’une pile Afin d’aborder le concept de piles, nous allons programmer la factorielle en utilisant les piles, et voir comment PROLOG utilise les piles. Mathématiquement on défini cette fonction par fact : N -> N de N dans N 0 -> 1 0! = 1 n -> n *(n-1)! n! = n * (n-1) ! Il est possible d’utiliser une syntaxe très proche en PROLOG. Programme : /* Calcul de factorielle en utilisant les piles */ fact(0,1). fact(X,Y):-X>0 , X1 is X-1 , fact(X1,Z) , Y is Z*X. Application : Calcul de 5! ?- fact(5,Y). Y = 120 ; No PROLOG calcule 5! Et il ne trouve bien qu’un seul résultat à cette requête : 5! = 120. Cette façon de programmer factorielle a théoriquement un inconvénient car pour calculer n! on utilise une pile de hauteur n ce qui n’est pas forcément recommandé. En effet, le principe du programme est de stocker n, n-1, …1 dans une pile puis d’en faire la multiplication. Passons en mode debug afin de voir ce qu’il se passe lorsque PROLOG calcul 5! Nous avons auparavant mis un Spy Point sur le prédicat fact/2 en utilisant l’interface graphique de SWI PROLOG. Le mode debug va nous permettre de visualiser, et ainsi de comprendre le concept de piles . Application : Calcul de 5! en mode debug [debug] [1] 18 ?- fact(5,Y). T Call: (14) fact(5, _G678) T Call: (15) fact(4, _G758) T Call: (16) fact(3, _G761) T Call: (17) fact(2, _G764) T Call: (18) fact(1, _G767) T Call: (19) fact(0, _G770) T Exit: (19) fact(0, 1) T Exit: (18) fact(1, 1) T Exit: (17) fact(2, 2) T Exit: (16) fact(3, 6) T Exit: (15) fact(4, 24) T Exit: (14) fact(5, 120) Y = 120 % Spy point removed from fact/2 Au cours des 6 premières lignes du traçage, on peut voir les appels récursifs à la règle « fact(X,Y):-X>0 , X1 is X-1 , fact(X1,Z) , Y is Z*X. » avec son premier argument qui est décrémenté à chaque fois et le niveau de l’appel (entre parenthèses) qui augmente. Sur ces mêmes lignes, le deuxième argument est une variable interne sans valeur. Ce n’est qu’une fois qu’on a atteint la règle « fact(0,1). » que PROLOG fait le calcul de 5! , sur les 6 dernières lignes, en dépilant les niveaux d’appel qui contiennent les valeurs 5, 4, 3, 2 et 1. On voit donc ici très clairement le concept de piles. De plus cela montre que c’est un aspect fort et très présent dans PROLOG, car il intervient directement dans le calcul et la résolution des problèmes posés. Pour aller plus loin dans la compréhension de l’omniprésence des piles, il faut savoir que PROLOG utilise nécessairement deux piles (une pile de buts et une pile d’environnement) pour exécuter un programme. Ainsi, la liste des entiers n, n-1, …, 1est stockée dans la pile d’environnement et ne nécessite pas la création d’une pile dédiée. Pour trouver une preuve et afficher la solution associée, PROLOG utilise deux piles de piles : La pile des buts dans laquelle il stocke tous les niveaux de buts qu’il a cherché à atteindre. Un niveau de buts est lui-même représenté par une pile de buts qui contient toujours au moins un but sauf lorsqu’on a atteint la fin de la démonstration (on peut alors retourner le résultat en cas de succès ou non sinon). Une preuve est donc l’ensemble des buts par lesquels on est passé avant d’obtenir une pile de niveau de buts vide. La pile d’environnement est elle aussi une pile de piles car à chaque niveau de buts est associée une pile d’environnement de niveau de buts. PROLOG stocke dans chacune de ces sous piles les variables intervenues dans l’unification qui l’a amené à ce niveau. Dans la pile d’environnement, il conserve donc toutes les variables qui ont été utilisées pendant la démonstration. Elle lui sert ainsi à retrouver le résultat de la preuve en cas de succès.