Patrice Bailhache
A la recherche d’un (impossible)
démonstrateur intelligent
Acta Universitatis Lodziensis. Folia Philosophica nr 9, 133-144
1993
A C T A U N I V E R S I T A T I S L O D Z I E N S I S
F O L I A P H I L O S O P H I C A 9 , 1993
Patrice B ailhache
A LA RECHERCHE D’UN (IMPOSSIBLE)
DÉMONSTRATEUR INTELLIGENT
Le d év elo p p em e n t de l'in fo rm a tiq u e a p e rm is l’esso r, ces d e rn iè re s a n n ées, d e n o m b re u x logiciels d 'a id e à l ’e n se ig n e m e n t de la lo g iq u e, sin o n en F ran c e , d u m o in s d a n s les p ay s a n g lo -sax o n s. La p lu p a rt de ces logiciels, d ès q u 'il s’ag it d u calcul des p ré d ic a ts (d u p re m ie r o rd re , avec o u san s id e n tité ), fo n c tio n n e n t cn sim ples vérificateurs, c 'e st-à -d ire q u e le rôle de la m a c h in e se tro u v e ré d u it à c o n trô le r q u e les d é d u c tio n s p ro p o sé es p a r l'u tilis a te u r so n t c o rre c te s. Q u 'ils fo n c tio n n e n t ainsi, et n o n p a s co m m e des d ém onstrateurs, se c o m p re n d facilem ent: d 'a p rè s le th é o rè m e d 'in d é c id a b ilité , il ne p eu t ex ister d 'a lg o rith m e g én éral p o u r le calcu l des p ré d ic a ts, de s o rte q u e l’é c ritu re d ’u n p ro g ra m m e est th é o riq u e m e n t im p o ssib le p o u r la d é m o n stra tio n .
M ais o n sait to u t de m êm e q u e ie p ro b lè m e de la d écision e st so lu b le p o u r c erta in es classes de fo rm u les. En o u tre , d a n s de n o m b re u x c as p lu s o u m o in s sim ples, on c o n s ta te q u 'u n logicien de force m o y en n e tro u v e a isé m e n t la « b o n n e d éd u ctio n » . O r ce q u i est aisé in fo rm e llem en t se révèle so u v e n t difficile dès q u 'o n c h erch e à le fo rm alise r, et plus e n co re dès q u 'o n v e u t le p rogram m er.
Les tra v a u x d a n s le d o m a in e de la d é m o n s tra tio n a u to m a tiq u e so n t n o m b re u x . A vec l'a p p a ritio n d u lan g ag e Prolog, l'u sa g e d es clau ses de H o rn s'e st é te n d u . C e p e n d a n t, cela n 'e s t p as s a tisfa is a n t p o u r un logiciel d 'a p p re n tis s a g e de la lo g iq u e, q u e l'o n v o u d ra it v o ir fo n c tio n n e r en v é rita b le
d ém onstrateur gén éra l intelligent, q u i ne se lim ite p as à u n e s tru c tu re
p a rtic u liè re de fo rm u le s co m m e celle des clau ses de H o rn . C 'e st p o u rq u o i, n o ta m m e n t, j'a i c h erch é à c o n str u ire un tel d é m o n stra te u r .
134 P a tric e B a ilh a c h e
1. « I N T E L L I G E N C E » E T « N A T U R E »
Q u e lq u es e x am p les sim ples - je vais en d o n n e r b ie n tô t - fo n t ra p id e m e n t c o m p re n d re ce q u 'il fa u t e n te n d re p a r Y intelligence d a n s u ne p re u v e lo g iq u e, d u m o in s p o u r u n e p re m iè re a p p ro c h e n o n d étaillée (la d é fin itio n p récise d u c o n ce p t e st c e rta in e m e n t b e a u c o u p p lu s délicate, v o ire m êm e im p o ssib le, p ré c isé m e n t d 'a p rè s ce q u e n o u s a enseigné G ö d el).
P re n o n s ain si la fo rm u le: 3.yVv F x y з Vv3.y F xy.
Sa p re u v e d a n s le systèm e de deduction naturelle de G e n tz e n s'a d m in is tre san s d ifficu lté. A p rè s a v o ir a p p liq u é la règle d 'a n a ly s e d u fo n c te u r im plication. o n u tilise les règles c o n c e rn a n t les q u a n tific a te u rs:
D éduction «intelligente»
1. => 3.vVy F x y з Vv3.v F x y —,
2. 3.vVr F x y => Vy3.v F x y g —, x j a v a r ja b le n o u v elle
3. Vv F ay => Vv3.y F x y —. \/r’/A v a ria b le nouvelle
4. Vv Fay => 3.Y F x b y —, y t y v a ria b le an cien n e
5. Vv Fay. Fab => 3.y F x b —, j x / a v a rja ble an cien n e
6. Vv Fay, Fab => 3.y F x b , Fab séq u en ce valide
Bien e n te n d u , d a n s c ette d é d u c tio n , le je u d u ch o ix des v a ria b le s libres q u i a p p a ra iss e n t p a r l'a p p lic a tio n des règles d ’a n aly se des q u a n tific a te u rs est essentiel. A insi les règles => V et 3 => n 'a u to rise n t-e lle s q u e l'em p lo i de v a ria b le s nou v elles, ta n d is q u e les d eu x a u tre s p e rm e tte n t th é o riq u e m e n t celui de n ’im p o rte q u elle v a ria b le 1, m ais d o iv e n t en fait, p o u r des raiso n s d ’é lé m en ta ire s tra té g ie, ê tre re stre in te s aux v a ria b le s lib res q u i fig u ren t d éjà d a n s la d é d u c tio n 2.
M ais a u d e là de ces re stric tio n s, o n c o n sta te q u e p lu sieu rs ch o ix intelligents o n t été p ra tiq u é s d a n s c ette preuve:
1. Les d eu x règles =>V et 3 => o n t été a p p liq u é es a v a n t les d eu x a u tre s =>3 et V =>, c 'e st-à -d ire q u e les v a ria b le s libres no u v elles o n t été dégées a v a n t q u ’elles s o ien t e m p lo y ées c o m m e v a ria b le s a n cien n es p a r les règles =>3 et V=>.
2. Le ch o ix des v a ria b le s an cien n e s, d a n s les d eu x d e rn ie rs p as, n ’a p a s été q u e lc o n q u e , m ais a é té p ra tiq u é de telle s o rte q u e la fo rm u le Fab figure des d eu x c ô té s de la flèche de la séq u en ce, p o u r q u e celle-ci a ch èv e la d é m o n st ra tio n .
1 O n d o i t to u te fo is é v ite r les v a r ia b le s d é jà q u a n tifié e s , a u ris q u e d e c o m m e ttr e d es « c o llis io n s » d e q u a n t i f i c a t e u r s , c o r r e s p o n d a n t à d e s s o p h is m e s .
2 L a n é g lig e n c e d e ce s e c o n d i m p é r a ti f c o n d u ir a it à d e s s é q u e n c e s n o n c o n c lu siv e s , s a n s r a p p o r t a v e c la n a t u r e d e la fo rm u le . P a r ex e m p le , l'e m p lo i d e s v a r ia b le s c e t d d a n s les d e u x d e r n ie rs p a s d e la p re u v e p r o d u i r a i t la s é q u e n c e : V r F a y, F a c => Эх F x b , Fdb.
A fin de m ieux p e rc ev o ir la p o rté e de ces d eu x m o d e s d e la p ro c é d u re , 011
p e u t c o m p a re r la d é d u c tio n «intellig en te» avec la d é d u c tio n q u e j ’ap p clcrai « p lanifiée» o u « sy sté m a tiq u e » , e t q u i co n siste, en fa it, en u n e a n aly se en largeur
d 'a b o rd de l'a r b re de d é d u c tio n . C ette d é d u c tio n p ro c è d e p a r étapes, en
c h a c u n e d esq u elles e x ac te m e n t u ne règle se tro u v e a p p liq u é e (si c ’e st p o ssib le) à c h a q u e fo rm u le de la séq u en ce du d é b u t de l’é ta p e 3. D éduction «planifiée» E T A P E 1 ch em in 1 1. => 3„yVv F x y з Vy3.Y F x y => ZD 2. 3xVy Л гу => V)'3.Y F x v E T A P E 2 ch em in I 2. 3.vVy F x y => Vy3-Y F x y . 3 => x / a v a ria b le n o u v elle 3. Vv F a y => Vi 3.Y F x v w ,, . . .
=> V y/о v a ria b le n o u v elle 4. Vy F ay => 3.Y F xb
E T A P E ’ 3 c h em in 1
4. Vy F av => 3.Y F x b w , . . .
V => y / a v a ria b le a n cien n e
5. Vy Fav, Faa => 3.Y F xb ..
V => y /b v a ria b le an cien n e
6. Vy Fav, Fab, Faa => 3.Y F x b , . , ,
=> 3 x ja v a ria b le a n cien n e
7. Vy Fay, Fab, Faa => 3.Y F xb , Fab séq u en ce valide
O n c o n s ta te u n c h a n g e m e n t avec la d é d u c tio n in te llig e n te à la fo rm u le 5, d a n s laq u elle la fo rm u le Faa est p ro d u ite in u tile m e n t, m ais ré g u liè re m e n t, c a r la p la n ific a tio n exige n o ta m m e n t q u e so ien t tirées to u te s les in sta n ce s po ssibles, avec les v a ria b le s libres d is p o n ib le s, des fo rm u le s u n iverselles v raies (o u existen tielles fausses). L ’e x am p le ch o isi ici est d u reste tro p sim p le, c a r la
m aladresse p ro v o q u é e p a r la p la n ific a tio n reste très lim itée. U n e a u tre
m a la d re sse p o u r r a it ê tre q u e les règles =>3 e t V=> so ien t e m p lo y é es a v a n t les règles => V et 3 =>, a lo rs q u e l’inverse s e ra it e ffectiv em en t p o ssib le4.
N o to n s q u ’il est d ’u sag e de q u a lifie r de n a turelle le style de d é d u c tio n «à la G e n tze n » , illu stré ici a u ta n t p a r la d é d u c tio n in te llig e n te q u e p a r la d é d u c tio n
C e lte p ro c é d u re p la n ifié e est d é fin ie p a r S . C . K l е е n e . a u c h a p i tr e 6 d e s a ü ig iijiie
n u ilh é m a tiq u e (A . C o lin . P a ris 1971. p. 2 89 3 1 0 d e la tr a d u c t io n fra n ç a ise ).
4 II f a u t te n ir c o m p te d u fa it q u e d e s fo r m u le s d u g e n r e ЗлЛЛ· F x y p e u v e n t trè s b ie n fig u re r à la d r o ite d e la flèc h e d e s sé q u e n c e s , a u q u e l c a s la rè g le => 3 se tro u v e n é c e s s a ire m e n t a p p liq u é e a v a n t la rè g le =>V (d u m o in s e n ce q u i c o n c e rn e c e tte fo rm u le ), c 'e s t- à - d ir e q u ’u n e v a r ia b le lib re n o u v e lle se t r o u v e n é c e s s a ire m e n t d é g a g é e a p r è s l’e m p lo i d e telles v a r ia b le s p o u r les u n ific a tio n s d e fo rm u le s. C eci, o n le s a it, p e u t m e n e r à d e s c h e m in s in fin is.
1 3 6 P a tric e B a ilh a c h e
planifiée. C e q u a lific a tif p ro v ie n t d u fait q u e, p a r c o n tra ste , les p reuves a x io m a tiq u e s q u i u tilise n t la règle M o d u s P o n e n s (o u règle de D éta ch em en t) o n t u ne s tru c tu re e n tiè re m e n t in d é p e n d a n te de celle de la fo rm u le à p ro u v e r5. En q u e lq u e so rte , la c o m b in a iso n de la règle de su b stitu tio n et de la règle M o d u s P o n e n s a n n ih ile to u te m ém o ire de la fo rm u le. M ais o n d é co u v re, p o u r ainsi d ire , q u e la n a tu re n 'e st n u lle m e n t intelligente! Si e ffectiv em en t la d é d u c tio n n a tu re lle fo u rn it sy sté m a tiq u e m e n t, san s e ffo rt d 'im a g in a tio n , une p re u v e de n 'im p o rte q u elle fo rm u le v alide, en rev a n ch e elle ne d o n n e , dès q u 'il s 'a g it d 'u n e ex p re ssio n ta n t soit p eu co m p lex e, q u 'u n e m auvaise preu v e, lo n g u e, rem p lie de p as in tu tiles. L a d é d u c tio n n a tu re lle ne ré so u t d o n c n u lle m e n t le p ro b lè m e de la stratég ie. Il fau t se c o n te n te r de d ire q u ’elle le pose en certa in s term es, san s d o u te p lus clairs q u ’avec les a u tre s styles de systèm es. L 'o m b re de G ö d e l se p ro je tte ici de to u te sa g ra n d e u r: p u isq u e le calcu l des p ré d ic a ts n 'e s t p as d écid ab le, b ien q u e co m p le t, il ne fa u t rien a tte n d re de plus d 'u n e d é d u c tio n naturelle p a r essence in c a p ab le de to u t p o u v o ir de décision.
2. A LA R E C H E R C H E D E L '( I M P O S S I B L E ) IN T E L L I G E N C E
Les d e u x c ritè re s é n o n cés ci-d essu s p o u r la p ro c é d u re in tellig en te d o iv en t m a in te n a n t ê tre dév elo p p és.
I. E n ce qu i c o n c e rn e la p réséan ce de l'a p p lic a tio n des règles => V et 3 => s u r les règles => 3 et V=>, seule u n e v ision sim plifiée des ch o ses p e u t laisser p e n se r q u e la situ a tio n est sim ple. E n réalité, co m m e je l’ai m e n tio n n é en n o te, la s tru c tu re des fo rm u les à tr a ite r p e u t fo rcer à l’a p p lic a tio n d a n s l'o rd re inverse, et il ne reste p lu s q u ’à se s o u m e ttre a u v e rd ic t des d o n n é es. M ais m êm e si l'o n ne se tro u v e p a s d a n s ce d e rn ie r cas, la situ a tio n p e u t ê tre tru ffée d 'a m b ig u ïté s: il p e u t très bien y a v o ir c o n c u rre n c e e n tre p lu sie u rs a p p lic a tio n s d es règles d u p re m ie r g ro u p e e t/o u c o n cu rre n ce e n tre p lu sie u rs a p p lic a tio n s des règles d u seco n d g ro u p e . O n ne v o it g u ère quelle (m éta-)règ le gén érale a d o p te r p o u r tra n c h e r d a n s ces o p tio n s.
E n o u tre , si c’est le cas, c 'e st-à -d ire si p a r ex em ple d es fo rm u les d u genre Зл-Vv F x y , 3.\'3fV c G x y :,... fig u ren t à la d ro ite de la flèche d e la séq u en ce, il fa u t a d o p te r u n e ligne de c o n d u ite qu i p e rm e tte de d é g ag e r aussi vite que p o ssib le les v a ria b le s libres n o uvelles. Il est b ien c la ir q u e c ette ligne de c o n d u ite d ev re ê tre de tra v a ille r s u r de telles fo rm u les (su r leu rs q u a n tific a te u rs existen tiels p o u r celles de d ro ite ) a v a n t d ’a p p liq u e r les m êm es règles à des fo rm u le s «cu l-d e-sac» (co m m e 3.v F x), q u i ne c o n d u ise n t p a s à des e x p ressio n s d é g a g e a n t en su ite des v a ria b le s n o uvelles. E t d a n s cette voie, on p o u rr a m êm e
5 P a r e x e m p le , d a n s les sy s tè m e s a x io m a tiq u e s p o u r le c a lc u l d e s p r o p o s itio n s d e R u ssell o u d e L u k a s ie w ic z .
é ta b lir u ne h ié ra rc h ie stra té g iq u e: tra ite r p a r o rd re de p rio rité d é c ro issa n te les fo rm u le s de s tru c tu re (à d ro ite de la flèche):
Эх F x. 3xVv F x y . 3 x 3 jV z G x yz, 3x3v3zV u· H x y z w ,...
A v o u o n s c e p e n d a n t q u e, si d ’une m a n iè re g én érale c ette ligne de c o n d u ite p a ra ît fo n d ée, rien n ’a ssu re to u te fo is q u ’elle se m o n tre r a p a rfa ite m e n t in te l lig en te d a n s to u s les cas d ’esp èce6.
2. Le seco n d c ritè re p o u r la p ro c é d u re in te llig e n te est celui d u ch o ix des v a ria b le s an cien n e s, a u tre m e n t d it celui d e Y unification des fo rm u le s a to m iq u es. Ici, u n a lg o rith m e e st c o n n u : c ’est celui de la d é te rm in a tio n d u p lu s g ra n d
unificateur. J ’ai c h erch é, p o u r un logiciel d ’en seig n em en t d e la d é d u c tio n
n a tu re lle , à faire à p eu p rés la m êm e ch o se p a r u ne p ro c é d u re sim plifiée, m ais m o in s sy sté m a tiq u e , o ù l’u n ifica tio n a lieu en d eu x tem p s. D a n s u n p re m ie r tem p s, l’u n ifica tio n est faite p a r c o m p a ra iso n des a to m e s de la fo rm u le à in s la n tie r avec ceux des a u tre s fo rm u les de la séq u en ce. A u c o u rs de cette éta p e, les in s ta n tia tio n s p ro d u is a n t des a to m e s san s a u c u n e v a ria b le liée o n t la p rio rité s u r les a u tre s 7. D a n s un seco n d tem p s, le ch o ix d es v a ria b le s a n cien n e s est « affiné» p a r la c o m p a ra iso n , n o n p lus d e sim ples fo rm u le s a to m iq u e s, m ais d e v é rita b le s so u s-fo rm u le s. U n ex em p le8 fe ra c o m p re n d re la n écessité d e cette seco n d e «passe».
S u p p o s o n s q u e l’o n veuille p ro u v e r l’in c o m p a tib ilité lo g iq u e des tro is ex p ressio n s:
1. Эл-Vv· F x v
2. V.vV)6z (F x y з ( ( ~ F x z & F :y ) V (F yz & F zx))) 3. V x 3 y V z ~ ( fy z & F zx)
S an s d écrire le d é ta il d e la p ro c é d u re de la d é d u c tio n n a tu re lle d a n s le style de G e n tz e n , n o u s p o u v o n s a b ré g e r les écritu re s en tir a n t les in sta n ce s su iv an tes:
4. Vy F ay (d e 1 avec a v a ria b le n o uvelle)
5. 3 r V z ~ (F yz & Fza) (d e 3 avec a v a ria b le an cien n e )
6. V z ~ (F b z & Fza) (de 5 avec b v a ria b le n o uvelle)
7. Y j'3 z (ftïv з ( ( ~ F a z & F z y )V (F y z & Fza))) (de 2 avec a v a r. a n cien n e) 8. 3 z (F a b = > ((~ Faz & F zh )V (F b z & Fza))) (de 7 avec Λ v ar. an cien n e ) 9. Fab => ( ( ~ Fac & F c b )V (F b c & Fca)) (d e 8 avec c v a ria b le an cien n e )
6 11 f a u l n o t e r q u e c e g e n r e d e d iffic u lté e s t é lu d é d a n s le c a lc u l d e s p r é d ic a ts a v e c f o n c t i o n s d e
term e s. C a r a lo rs . les fo r m u le s p re n e x e s a v e c d e s q u a n tif ic a te u r s u n iv e rs e ls p la c é s d a n s la p o r té e de
q u a n tif ic a te u r s ex is te n tie ls (p o u r u n e fo r m u le s itu é e à d r o i t e d e la flèche), s o n t re m p la c é e s p a r des fo rm e s d e S k o le m . ce q u i re v ie n t à les « p r é - in s ta n tie n d a n s u n o r d r e d o n n é . C f. p a r e x e m p le . J. P. D e l a h a y e . O u tils lo g iqu es p o u r /'in te llig e n c e a r tific ie lle , E y ro lle s . P a ris 1987. p . 127 e t su iv .
7 C ’e s t-à -d ire les i n s ta n t ia t io n s q u i p ro d u is e n t d e s fo rm u le s a to m iq u e s c o m m e F ab. e t n o n c o m m e 3x F x a . J ’a p p e lle in s ta n tia tio n l’a p p lic a tio n d e l’u n e d e s q u a t r e règles c o n c e r n a n t les q u a n tif ic a te u r s . E n l’o c c u rre n c e , il s ’a g it d e s i n s ta n t ia t io n s u tilis a n t d e s v a r ia b le s a n c ie n n e s .
8 T . d e Q u i n e , M é th o d e s de lo g iq u e, c h a p . 29, A . C o llin , P a ris 1973, (p . 175 d e la tra d , fra n ç a ise ).
1 3 8 P a tric e B a ilh ach e 10. ľa h 11. Fac 12. Ч F b c & F c a ) (de 4) (dc 4) (de 6)
Les fo rm u les 9, 10. 11. 12 é ta n i lo g iq u e m e n t in c o m p a tib le s, la p reu v e est achevée. L 'essen tiel q u i n o u s intéresse ici est le p assag e de la fo rm u le 7 à la fo rm u le 8. Le ch o ix de la v a ria b le an cien n e h est lait p a r u n ifica tio n d e la so u s-fo rm u le Fbz & F za de 8 avec c elle m êm e so u s-fo rm u le d a n s 6. E v id em m en t. la g estion in fo rm a tiq u e de ces o p é ra tio n s d ev ien t p a ssa b le m e n t c o m p lexe. A titre in d ic a tif, je d o n n e en an n ex e, la p a rtie de p ro g ra m m e pascal qui réalise l'u n ific a tio n d a n s le logiciel q u e j 'a i m e n tio n n é . E t je m 'a d re sse à qui v eut, p o u r c a lla b o re r d a n s le p e rfe c tio n n e m e n t de l'a lg o rith m e in fo rm a tiq u e de ce g en re d 'u n ific a tio n .
En défin itiv e, bien q u e la voie «intellig en te» soit so u v en t m an ifeste p o u r la d é d u c tio n des fo rm u les les p lu s c o u rte s et les plus b a n ales (en co re q u ’il a rriv e fréq u e m m e n t q u 'u n é tu d ia n t de force m o y en n e ne les voie p as), à e x a m in e r la q u e stio n de p lus près, o n s 'a p e rç o it q u e les p ro b lè m e s p o sés so n t très difficiles, s an s p a rle r de la m ise en o e u v re in fo rm a tiq u e , q u i d ev ien t vite ép in eu se. C ela est. si l'o n v eu t, u ne co n sé q u e n ce d irecte de cet é ta t de ch o ses lo g iq u e, m is en lum ière p a r G ö d el: le calcul des p ré d ic a ts bien q u e co m p lcs. n 'e st p a s déciso ire. D e là résu lte q u 'u n a lg o rith m e de d é d u c tio n p lan ifiée est re la tiv e m e n t facile a écrire, m ais q u 'e n rev a n ch e la d e d u c tio n intellig en te réclam e im a g in a tio n , essais et «brico lag es» , avec en prim e - si j ’ose m e p e rm e ttre c ette v u lg a rité - la c e rtitu d e q u 'o n ne l'a tte in d ra ja m a is.
P O S Z U K I W A N I E P R O C E D U R Y I N T E L I G E N T N E G O D O W O D Z E N I A T W I E R D Z E Ń
W o s ta tn ic h la ta c h w r a z z ro z w o je m n a u k k o m p u te ro w y c h , p o ja w iło się w iele p ro g r a m ó w in ajatĄ c h w s p o m a g a ć n a u c / a n i e lo g ik i. W ię k s/o .sć / łych p ro g ia m o w slu/.y d o s p iu w d /а м іа ra c h u n k ó w , a n ie d o d o w o d z e n ia tw ie rd z e ń , p o n ie w a ż z g o d n ie ze z n a n y m tw ie rd z e n ie m G o d ła , nie istn ie je p r o c e d u r a ro z s trz y g a ln o ś c i tw ie rd z e ii ra c h u n k u p ie rw s z e g o rz ę d u . K ilk a m e la tw ie rd z e ń . w k tó ry c h jed n y m je s t tw ie rd z e n ie G o d ła , t l u m a c /y d la c z e g o d y s p o n u je m y d o b ry m i s y s te m a m i d e d u k c ji n a tu r a ln e j, m im o że la k t r u d n o j e s t {a fa k ty c z n ie n ie m o ż n a ) z n a le ź ć ..in te lig e n tn ą " p ro c e d u rę d o w o d z e n ia fo r m u ł. W a r ty k u l e p rz e d s ta w io n o d ro g ę u z y s k a n ia cz ę ś c io w e g o sy ste m u d o w o d z e n ia tw ie rd z e ń za pom oci} p ro c e d u ry u n ifik a c ji, d la k tó re j z a łą c z o n o p r o g r a m k o m p u te ro w y w ję z y k u p a s c a l.
U n iv e r s ité d e N a n te s F ra n c e
(i n tè g re le s v a ri n s tp u re au d é b u t de la li st e d es v a ri n s t) fo r t: = n b rv a ri n s t d o w n to 1 do v a ri n s t[ t + n b rv a ri n s tp u re ]: = -v a ri n s l[ t] : fp r t: = l to n b rv a ri n s tp u re do v a ri n s t[ t] : = v a ri n s tp u re [t ]; n b rv a ri n s t: = n b rv a ri n s t + n b rv a ri n s tp u re ; (s u p p ri m e le s v a ri a b le s qu i fi g u re n t p lu si e u rs fo ls ) t: = 2;\ vhi le t< = n b r \a r in s t d o b e g in lo r u: = I to t- ! do if v a ri n s t[ tj = v a ri n s t[ u ] th e n b e g in fo r lt: = t to n b r v a r in s t-I do v a ri n s t[ tt ]: = v a ri n s t[ ti + 1) ; d o c (n b rv a ri n s t) ;g o to v a ri n s ts u iv : e n d ; in c (t ); v a ri n s ts u iv ; e n d ; (S ec on d c ritè re de d é te rm in a ti o n d es c o n s ta n te s d ’i n s ta n ti a ti o n : p ro p o se s e u le m e n t un c la s s e m e n t d if fè re n t p o u r le s \a ri n s t d éjà tr o u v é e s c i-d e s s u s ) u: = 0 ; (f a it la li st e d es f o rm u le s a u tr e s q u e ) k: = k w h il e FH '[ k ]< > ‘" do (E c o n te n a n t au m o in s un e c o n s ta n te .) b eg in (e n le s a p p e la n t FC[ ]) F : = FG “ [k ]; if F < > E th en fo r t: = l to n b rv a ri n s t do if p o s (v a ri n s t[ t] .F )< > 0 th e n b e g in while (c o p y (F .l .l ) = ‘$ ') o r (c o p y ( F .l . I ) — T ) do F : = c o p y (F .3 .1 e n g th (F ) 2 ); in c (u ); F C ' [u] : = F ;go to s o rt ic G e n d ; s o rt ie G : in c (k ) e n d ; k. = l; w h ile F D * [k J< > " d o b e g in F : = FD * [k ]; if F < > E th en for l: = l to n b rv a ri n s t do if p o s (v a ri n s t[ t] .F )< > 0 th e n b e g in
