1L’élaboration de situations didactiques intégrant l’informatique pose toute une série de questions qui s’insèrent naturellement dans les différents cadres théoriques développés par les chercheurs en didactique des mathématiques, et en particulier celui de la théorie des situations. Au cœur de cette problématique se situe la question des choix didactiques impliqués dans la conception des logiciels et de l’analyse des liens complexes qui s’établissent entre le didactique et l’informatique.

2Ce texte porte sur une recherche visant à utiliser l’interaction avec un moteur d’inférence comme source d’activités d’apprentissage et d’enseignement sur les mécanismes logiques du raisonnement déductif et de la démonstration. Ce projet a donné lieu à la création d’un logiciel, appelé RAISON (Côté, 1996), et à deux expérimentations dans le cadre d’un cours universitaire offert à de futurs enseignants de mathématiques de niveau secondaire. Ce texte présente et analyse les grandes lignes d’une séquence d’activités avec ce logiciel. La séquence comprend trois sections qui chacune est structurée en épisodes. Ces sections représentent trois niveaux d’utilisation du logiciel.

Partir d’une simple interrogation sur ce qu’est raisonner

3E1 : On part d’une situation où on veut enseigner à un ordinateur à « raisonner ». On se demande : « Comment pourrait-on formuler une situation de raisonnement à partir de ce dessin ? »

4On interprète ce dessin comme contenant des objets géométriques, des points et une droite, qui ont certaines relations entre eux. On se demande comment « raisonner » dans cette situation, et en fait, ce que c’est « raisonner ». En s’aidant possiblement des définitions d’un dictionnaire, on arrive à poser qu’un raisonnement est une suite d’énoncés qui s’enchaînent selon certaines règles et aboutissent à une conclusion.

5À partir de la figure, on peut formuler des énoncés comme :

A est un point.
d1 est une droite.
C est sur d1.
B n’est pas sur d1.
B et E sont de part et d’autre de d1.

6On introduit l’idée que, dans sa forme la plus simple, un énoncé (ou une proposition) est quelque chose qu’on affirme et que cette affirmation réfère normalement à un ou à plusieurs objets. Par exemple, on affirme que les objets « B » et « E » sont de part et d’autre de l’objet « d1 ». On appelle prédicat ce qui, dans un énoncé, est affirmé. Ici le prédicat est « sont de part et d’autre de ».

7Le logiciel RAISON permet d’entrer dans la mémoire de l’ordinateur une banque d’énoncés. Pour entrer un énoncé, il faut le simplifier au point de n’avoir que le prédicat (en un seul mot) et ses objets, et suivre la convention que le premier terme est le prédicat. Ainsi les prédicats « est un point » et « sont de part et d’autre de » peuvent être simplifiés en « point » et « part_autre » et les énoncés « A est un point » et « B et E sont de part et d’autre de la droite d1 » deviennent dans l’ordinateur :

point A
part_autre {B E} d1

8Dans un énoncé, un objet peut être un mot (suite de caractères sans espace) ou un ensemble de mots (suite de mots entourée de crochets). Un ensemble est un regroupement d’objets distincts caractérisés par le fait d’être « ensemble », indépendamment de leur ordre. Ainsi dans « part_autre {B E} d1 » on a le prédicat « part_autre » avec deux objets, l’ensemble {B E) et le mot « d1 ». Le fait d’utiliser un ensemble nous assure que l’ordinateur va reconnaître que B et E sont de part et d’autre de d1 quel que soit leur ordre. Pour l’ordinateur, « part_autre {B E} d1 » et « part_autre {E B} d1 » est le même énoncé car {B E} et {E B} réfèrent au même ensemble.

9Pour qu’il y ait raisonnement, il faut partir d’un certain nombre d’énoncés qu’on accepte, et en arriver à déduire logiquement un nouvel énoncé. On se demande ici quel pourrait être un exemple d’énoncé déduit à partir d’autres énoncés.

Analyse

• Le contexte général de ces activités est le rôle de la logique dans l’apprentissage de la démonstration. On veut amener progressivement l’étudiant à prendre conscience que, du point de vue de la logique, une démonstration est une sorte de calcul effectué sur des énoncés à partir de règles qui n’ont rien à voir avec la signification de ces énoncés.
• Cet épisode fait appel à des éléments de connaissance logiques, géométriques et informatiques. Les éléments géométriques servent de support ou de prétexte pour parler de logique. Les éléments informatiques apparaissent comme des contraintes attribuées à l’ordinateur, mais constituent en fait l’entrée dans une situation où le raisonnement deviendra l’application mécanique d’opérations sur des énoncés.
• L’élément central ici est la notion d’énoncé en tant que prédicat accompagné d’objets. Ces deux termes constituent les éléments fondamentaux à partir desquels le raisonnement sera constitué comme une forme de calcul. La représentation utilisée par l’ordinateur force l’utilisateur à penser en termes de prédicat et d’objets. Ce n’est pas « naturel ». Ce n’est pas nécessairement facile au début. Il faut réaliser qu’il y a une part de convention dans le choix des prédicats, du nombre et du type d’objets qu’ils mettent en relation. Certains choix sont plus « intéressants » que d’autres. Une fois qu’on a décidé d’une forme, il faut la conserver, sinon les raisonnements vont s’avérer hasardeux.

10E2 : La question de départ est : « Sachant que A et B sont du même côté de d1 et que B et E sont de part et d’autre, on peut déduire que A et E sont de part et d’autre. Comment peut-on amener l’ordinateur à effectuer ce raisonnement ? »

11On accepte au départ les énoncés suivants, que l’on fait entrer dans la banque d’énoncés :

12Pour déduire un énoncé à partir d’un ou de plusieurs autres énoncés, il faut utiliser une règle d’inférence. C’est une sorte de principe général qu’on peut appliquer dans un cas particulier. Comment la formuler ici ?

Si deux points sont du même côté d’une droite, et que l’un d’entre eux et un troisième point sont de part et d’autre de cette droite, alors l’autre des deux premiers et le troisième sont de part et d’autre de la droite.

13Une règle est plus facile à formuler si on nomme les objets en jeu :

Si les points X et Y sont du même côté de la droite d et que les points Y et Z sont de part et d’autre de d, alors X et Z sont de part et d’autre de d.

14Voici une façon d’utiliser cette règle pour déduire que « A et E sont de part et d’autre de d1 » :

• La règle s’interprète comme suit : si ton but est de prouver que les points X et Z sont de part et d’autre de la droite d, alors essaie de trouver un point Y tel que X et Y sont du même côté, et Y et Z sont de part et d’autre de d.
• On veut prouver que A et E sont de part et d’autre de d1. Donc dans notre cas, X = A, Z = E et d = d1.
• En regardant dans la banque, on découvre que A et B sont du même côté de d1. Donc on peut prendre Y=B.
• On voit ensuite dans la banque que B et E sont de part et d’autre de d1.
• Donc la règle peut s’appliquer et on a le droit de conclure que A et E sont de part et d’autre de d1.

15C’est comme cela que l’ordinateur « raisonne ». Il utilise les règles qu’on lui donne pour partir d’un énoncé à prouver et le relier aux énoncés acceptés au départ. La règle qui vient d’être utilisée peut être entrée dans l’ordinateur en tapant :

But : part_autre {?X?Z} ?d
Étape : prouve EX point ?X : même_côté {?X ?Y} ?d ET part_autre {?Y ?Z} ?d

16Ensuite, si on lui demande de prouver notre énoncé, il va afficher les traces suivantes :

But(1) : part_autre {A E} d1
Règle activée : part_autre {?X ?Z}?d
Étape #1 sur 1 : prouve EX point ?Y : même_côté {?X ?Y}?d ET part_autre {?Y ?Z} ?d
But(2) : EX point ?Y : même_côté {A ?Y} d1 ET part_autre {?Y E} d1
Valeurs possibles de ?Y : {A B E}
But(2) (Cas #1 sur 3) : point A
But(3.1) : même_côté {A} d1 ET part_autre {A E} d1
But(4a) : même_côté {A} d1
But(4a) : même_côté {A} d1 : valeur inconnue
But(3.1) : même_côté {A} d1 ET part_autre {A E} d1 : valeur inconnue
But(2) (Cas #2 sur 3) : point B
But(3.2) : même_côté {A B} d1 ET part_autre {B E} d1
But(4a) : même_côté {A B} d1
But(4a) : même_côté {A B} d1 : VRAI
But(4b) : part_autre {B E} d1
But(4b) : part_autre {B E} d1 : VRAI
But(3.2) : même_côté {A B} d1 ET part_autre {B E} d1 : VRAI
But(2) : EX point ?Y : même_côté {A ?Y} d1 ET part_autre {?Y E} d1 : VRAI
But(1) : part_autre {A E} d1 :VRAI

17La partie du logiciel qui permet d’effectuer ces opérations s’appelle un moteur d’inférence. Lorsqu’on lui donne un énoncé à prouver, il commence par vérifier si cet énoncé, ou sa négation, se trouve dans la banque. Si c’est le cas, il répond tout de suite VRAI ou FAUX. Sinon, il cherche à appliquer une règle. Ceci se produit s’il trouve une règle dont l’énoncé de but peut être pairé avec l’énoncé à prouver.

18Un pairage entre deux énoncés réussit si les termes constants du premier correspondent exactement aux mêmes termes, dans l’ordre, dans le second. Le logiciel attribue alors aux variables du premier les valeurs correspondantes dans le second. Par exemple, le pairage :

19réussit et donc l’attribution des valeurs se produit : ?X ← A, ?Z ← E et ?d d1.

20Lorsque ce pairage réussit, on dit que la règle en question est activée, et elle apparaît dans les traces. Cela signifie que les variables de l’énoncé de but sont remplacées par leurs valeurs dans la première étape de la règle et que cet énoncé devient le nouvel énoncé à prouver, le nouveau but :

But(2) : EX point ?Y : même_côté {A ?Y} d1 ET part_autre {?Y E} d1

21Le terme EX signifie « il existe », et les « : » se lisent « tel que ». Il faut maintenant prouver que parmi les valeurs possibles de ?Y qui correspondent à des points, il y en a une qui satisfait à la fois les énoncés « même_côté {A?Y} d1 » et « part_autre {?Y E} d1 ». En examinant la banque, le moteur trouve trois valeurs possibles pour la variable ?Y. Il essaie de prouver les énoncés avec ?Y=A et échoue au premier. Il essaie avec la seconde valeur, ?Y=B, et cette fois réussit car ces deux énoncés sont dans la banque. Ensuite le moteur conclut en remontant des buts 4 au but 3, puis 2, puis 1.

22Ce fonctionnement du moteur d’inférence correspond au processus appelé dans les travaux en intelligence artificielle chaînage arrière. C’est un procédé de déduction qui consiste à partir de l’énoncé à prouver et à utiliser les règles d’inférence pour revenir aux axiomes ou hypothèses. Nous verrons plus loin que le procédé inverse, le chaînage avant, peut aussi être programmé avec RAISON.

Analyse

• Le fait d’essayer de formuler une règle en français et de voir l’avantage de nommer les objets, conduit naturellement à introduire la notion de variable. Ensuite, sauf pour la syntaxe particulière des énoncés, on voit que la formulation d’une règle dans le logiciel est semblable à sa formulation en français.
• L’élément central de cet épisode est l’introduction du moteur d’inférence. Son fonctionnement nous fait entrer de facto dans une conception du raisonnement comme étant une sorte de calcul, un ensemble d’opérations effectuées mécaniquement sur des symboles. Le mécanisme du choix d’une règle appropriée est capté par les contraintes associées à l’opération de pairage et l’activation comme telle de la règle est un processus d’affectation de valeurs à des variables.
• La stratégie didactique consiste essentiellement à faire du moteur d’inférence un objet d’étude. La maîtrise graduelle de la formulation de règles en termes de but et d’étapes, puis du processus de décomposition d’un but en sous-buts et d’interprétation des relations d’implication lors de la remontée d’un but au but précédent, va aussi comprendre la rencontre avec certains concepts clés de la logique tels les connecteurs et les quantificateurs, les tautologies et contradictions. Ainsi on peut dire que d’une certaine façon le savoir est inscrit dans le logiciel. Mais pour y avoir accès, il faut interagir avec lui.
• L’outil central d’apprentissage est la production des traces. Le logiciel permet de choisir entre des traces complètes, avec tous les essais effectués par le moteur, ou abrégées, soit seulement les essais qui ont réussi. La trace permet d’« objectifier » un raisonnement. Elle constitue une représentation non seulement de la suite d’énoncés qui va des axiomes à l’énoncé à prouver (qui correspond à la « remontée » du moteur), mais aussi du processus de recherche parmi les axiomes et théorèmes pertinents.

23E3 : L’apparition des termes « EX » et « ET » dans l’épisode précédent sert de point de départ pour introduire les notions d’énoncé composé, de connecteur binaire, de valeur de vérité, de table de vérité et de quantificateur. Cet épisode comprend trois séries d’exercices.

241. — Le logiciel permet d’utiliser, en plus de la négation (NON), cinq connecteurs soit la conjonction (ET), la disjonction (OU), la disjonction exclusive (OUX), l’implication ( ») et la double implication (« »). On propose aux étudiants d’établir la table de vérité de chacun et de la vérifier à l’aide de l’ordinateur. On demande aussi de caractériser en quelques mots la définition de chacun des connecteurs.

25Les mots « VRAI », « FAUX » et « INCONNU » sont des mots réservés pour le logiciel. Ils permettent d’obtenir directement les tables de vérité inscrites dans le système, par exemple :

Prouve >> vrai OU faux
VRAI
Prouve >> inconnu ET vrai
Valeur inconnue
Prouve >> faux >> inconnu
VRAI

26On demande aussi de formuler la règle qu’utilise le logiciel pour interpréter les cas où une des valeurs est inconnue. Il y a place ici pour un travail sur le fonctionnement de chaque connecteur, et en particulier celui de l’implication.

272. — On explore le fonctionnement du logiciel lorsqu’on lui demande de prouver un énoncé simple contenant une ou plusieurs variables. On constate qu’il retourne l’ensemble des valeurs des variables pour lesquelles l’énoncé apparaît dans la banque. En d’autres mots, le moteur effectue un pairage entre l’énoncé à prouver et chacun des énoncés de la banque, et retourne l’ensemble des valeurs pour lesquelles le pairage a réussi.

28Par exemple, avec la banque :

29on obtient :

prouve >> point ?X
{A B C D E}
prouve >> est_sur  ? d2
{B D}
prouve >> est_sur ?1?2
{[C d1] [D d1] [B d2] [D d2]}

303. — Pour qu’un énoncé avec variables puisse être évalué comme étant VRAI ou FAUX, il faut « quantifier » ses variables. On introduit les quantificateurs universel (POURTOUT) et existentiel (EX) et leur syntaxe.

31Partant de la banque de l’exercice précédent, on demande de formuler les énoncés suivants selon les conventions du logiciel, de prédire et de vérifier sa réponse :

Il existe un point sur la droite d2.
Tous les points appartiennent à la droite d1.
Toute droite contient au moins un point.

…

32L’examen des traces permet de suivre le fonctionnement de l’interprétation des quantificateurs :

But(1) : POURTOUT droite ?d : EX point ?P : est_sur ?P ?d
Valeurs possibles de ?d : {d1 d2}
But(1) (Cas #1 sur 2) : droite d1
But(2.1) : EX point ?P : est_sur ?P d1
Valeurs possibles de ?P : {A B C D E}
But(2.1) (Cas #1 sur 5) : point A
But(3.1) : est_sur A d1
But(3.1) : est_sur A d1 : FAUX
But(2.1) (Cas #2 sur 5) : point B
But(3.2) : est_sur B d1
But(3.2) : est_sur B d1 : Valeur inconnue
But(2.1) (Cas #3 sur 5) : point C
But(3.3) : est_sur C d1
But(3.3) : est_sur C d1 : VRAI
But(2.1) : EX point ?P : est_sur ?P d1 : VRAI
But(1) (Cas #2 sur 2) : droite d2
But(2.2) : EX point ?P : est_sur ?P d2
Valeurs possibles de ?P : {A B C D E}
But(2.2) (Cas #1 sur 5) : point A
But(3.1) : est_sur A d2
But(3.1) : est_sur A d2 : FAUX
But(2.2) (Cas #2 sur 5) : point B
But(3.2) : est_sur B d2
But(3.2) : est_sur B d2 : VRAI
But(2.2) : EX point ?P : est_sur ?P d2 : VRAI
But(1) : POURTOUT droite ?d : EX point ?P : est_sur ?P ?d : VRAI

33On demande aussi d’expliquer dans quel cas un énoncé avec quantificateur va être évalué comme étant FAUX ou de valeur inconnue.

Analyse

• Le fait de tenir compte de la possibilité de ne pas connaître la valeur de vérité d’un énoncé correspond à ce qui peut se produire effectivement dans un contexte de démonstration et en même temps facilite l’analyse des caractéristiques de chaque connecteur.
• Dans l’approche décrite ici, les connecteurs et quantificateurs ne sont pas considérés comme des contenus de connaissance à maîtriser en tant que tels. Ce sont des outils qui interviennent dans la formulation des règles d’inférence et des énoncés à prouver. On verra plus loin que les tables de vérité servent principalement à justifier les règles logiques préprogrammées et que les différentes facettes souvent problématiques de l’interprétation de l’implication se retrouvent dans la justification des principes de démonstration.

Preuves et réfutations

34E1 : On continue à travailler avec des points et des droites et les diverses relations d’incidence. Par exemple, on peut se demander comment prouver qu’une droite en coupe une autre. Une règle possible est : deux droites se coupent si l’une contient deux points qui sont de part et d’autre de l’autre.

35On arrive ici à réaliser qu’une démonstration peut faire appel à plusieurs règles, et parfois à la même règle à plusieurs reprises. Une règle peut aussi comporter plusieurs étapes. Par exemple, il y a au moins deux façons de prouver que deux points X et Y sont du même côté d’une droite :

• S’il existe un point Z tel que X et Z, et Y et Z sont du même côté de la droite.
• S’il existe un point Z tel que X et Z, et Y et Z sont de part et d’autre de la droite.

36Lorsqu’une règle est activée, le moteur essaie la première étape. S’il ne réussit pas la preuve à ce niveau, il passe à la seconde étape, et ainsi de suite. On peut évidemment suivre cette démarche dans les traces.

37Lorsqu’on commence à travailler avec plusieurs règles et divers ensembles, on se retrouve facilement avec de très longues traces. On a à réaliser que la formulation des règles peut rendre une recherche plus ou moins efficace. En fait, les quantificateurs peuvent être vus comme des outils de programmation d’une recherche sur des ensembles de possibilités. Il y a essentiellement deux façons de contrôler cette recherche : prêter attention à l’ordre des quantificateurs, quand il y en a plusieurs, et surtout bien choisir les prédicats qui définissent les ensembles. Par exemple, au lieu de « EX point ?P : est_sur ?P d1 ET... », on peut écrire directement « EX est_sur ?P d1 : ... ».

38Après avoir exploré pendant un certain temps les différents aspects des raisonnements avec les prédicats « même_côté » et « part_autre », on peut en arriver à poser de façon générale le problème :

Étant donné un ensemble {P₁, P₂, ... P_n} de points n’appartenant pas à une droite donnée, quel est le nombre minimum d’énoncés utilisant les prédicats « même_côté » ou « part_autre » qu’il faut accepter pour être capable de prouver un des deux prédicats avec chaque couple possible de ces points ?

Analyse

39— On retrouve ici des éléments de connaissance qui relèvent de la géométrie, de la logique et de l’informatique. Les problèmes proposés donnent lieu à une réflexion géométrique et particulièrement à une prise de conscience des propriétés des relations « de part et d’autre » et « de même côté ». Pour faire raisonner l’ordinateur, il faut formuler les énoncés et les règles, donc utiliser correctement les quantificateurs et connecteurs, et développer une certaine compréhension de ce qui, dans le fonctionnement du moteur d’inférence, produit une démonstration. On se retrouve ici au cœur de ce qu’en informatique, on appelle la programmation logique.

40Ces trois aspects sont évidemment interreliés. Toute confusion à un niveau risque de se répercuter aux autres. Ceci peut possiblement augmenter la confusion, ou donner plus de chances de l’éclaircir. Par exemple, une certaine ambiguïté dans la formulation des règles d’inférence peut conduire à des raisonnements circulaires. Le moteur est programmé de façon à détecter les boucles, soit la tentative de prouver à un certain niveau un énoncé qui est déjà à prouver à un niveau précédent. Dans ce cas, le fonctionnement informatique devrait produire un questionnement au niveau de la définition des règles et de leur logique.

41— On peut distinguer quatre niveaux de sophistication dans l’utilisation du logiciel :

1. L’utilisateur recherche, parfois péniblement, à prouver un énoncé. Aussitôt qu’il obtient VRAI, il est satisfait et prêt à passer à une autre question.
2. L’utilisateur réalise que la réponse VRAI peut provenir d’un fonctionnement imprévu du moteur et que la seule façon de savoir s’il a vraiment démontré l’énoncé consiste à examiner la trace.
3. L’utilisateur réalise qu’il y a habituellement plusieurs façons de prouver un énoncé et s’intéresse à générer la plus simple, ou la plus rapide.
4. L’utilisateur s’intéresse aux propriétés (cohérence, possibilité de contradictions, ambiguïté...) du système défini par une banque d’énoncés et un ensemble de règles. Le dernier problème se situe à ce niveau.

42E2 : On s’intéresse maintenant à programmer RAISON pour qu’il puisse réfuter un énoncé. La façon la plus simple est évidemment d’introduire la négation de l’énoncé dans la banque. Par exemple :

Énonce >> NON est_sur A d1
Prouve >> est_sur A d1
FAUX

43Mais si on veut éviter d’avoir à introduire dans la banque toutes les possibilités de relation entre chaque point et chaque droite, il faut être en mesure d’introduire une règle permettant de déduire, par exemple, que si « A est sur d1 », l’énoncé « A et D sont de part et d’autre de d1 » est nécessairement faux.

44On a ici l’occasion de mettre en évidence le fait qu’une règle d’inférence qui sert à prouver un énoncé ne sert pas automatiquement à le réfuter. Les règles vues jusqu’à présent sont de la forme :

But : q
Étape : prouve p

45Si en essayant de prouver « p », le moteur obtient VRAI, il conclut que « q » est VRAI. Mais s’il obtient FAUX pour « p », que devrait-il conclure pour « q » ?

46Pour répondre à cette question, il faut comprendre le principe de démonstration à la base du fonctionnement du moteur d’inférence. Ce principe est connu traditionnellement en logique sous le nom de modus ponens. Selon ce principe, si on accepte à la fois l’énoncé « p » et l’énoncé « p implique q », on est obligé d’accepter l’énoncé « q ».

47Or entrer dans l’ordinateur une règle dont le but est « q » et l’étape « prouve p », c’est accepter l’énoncé « p implique q ». Aussi lorsque le moteur réussit à prouver « p », il peut accepter « q », puisque les deux conditions nécessaires pour appliquer le modus ponens sont satisfaites.

48Mais si « p » est FAUX, une des deux conditions n’est pas satisfaite et le modus ponens ne s’applique pas. C’est pourquoi le moteur passe alors à la règle suivante ou répond « Valeur inconnue ».

49Maintenant si on veut réfuter « q » en utilisant la règle du modus ponens, on a besoin d’accepter un énoncé de la forme « p implique NON q ». Le logiciel permet deux façons différentes d’entrer une règle de cette forme soit :

50Le premier cas conduit à entrer des règles différentes pour prouver et pour réfuter. Le second permet d’intégrer dans la même règle des étapes servant à prouver ou à réfuter. Le terme « prouve_réf p » signifie : « Si tu réussis à prouver p, alors q est réfuté, donc q est FAUX. »

51On peut donc construire une règle :

But : part_autre {?X ?Z} ?d
Étape : prouve_réf est_sur ?X ?d
prouve_réf est_sur ?Z ?d
prouve EX même_côté {?X ?Y} ?d : part_autre {?Y ?Z} ?d
prouve EX part_autre (?X ?Y} ?d : même_côté {?Y ?Z} ?d
prouve_réf même_côté {?X ?Z} ?d

52On a trois étapes qui servent à réfuter et deux qui servent à prouver. Et on peut choisir dans quel ordre elles vont être activées.

53Mais il reste une autre possibilité à envisager. On peut avoir une règle qui sert à la fois à prouver et à réfuter un énoncé. De quel type de règle s’agit-il ?

54Supposons qu’on veuille une règle permettant de prouver que trois points sont alignés. Comme trois points sont alignés s’ils appartiennent à la même droite, on peut formuler la règle :

But : alignés (?X ?Y ?Z)
Étape : prouve EX droite ?d : est_sur ?X ?d ET est_sur ?Y ?d ET est_sur ?Z ?d

55Cette règle permet de prouver et non de réfuter. Mais pour réfuter un énoncé avec « alignés », il faut montrer qu’il n’existe pas de droite qui contient les trois points. On a donc :

But : alignés {?X ?Y ?Z}
Étape : prouve_réf NON EX droite ?d : est_sur ?X ?d ET est_sur ?Y ?d ET est_sur ?Z ?d

56En fait la règle s’exprime sous la forme d’une double implication soit :

Trois points sont alignés si et seulement si ils appartiennent à une même droite.

57Le logiciel permet de créer une étape correspondant à une double implication en tapant par exemple :

But : alignés {?X ?Y ?Z}
Étape : prouve_et_réf EX droite ?d : est_sur ?X ?d ET est_sur ?Y ?d ET est_sur ?Z ?d

58Une étape commençant par « prouve_et_réf » signifie : si l’énoncé qui suit est VRAI, le but est VRAI. Si l’énoncé qui suit est FAUX, le but est FAUX.

59Pour simplifier le problème avec « alignés », on prend comme convention que si l’énoncé « est_sur P d » n’apparaît pas dans la banque, le point n’appartient pas à la droite. On peut donc introduire une règle qui va produire la réponse FAUX dans ce cas, soit :

But : NON est_sur ?P ?d
Étape : prouve VRAI

60Avec dans la banque les énoncés :

61on obtient :

But(1) : alignés {A F D}
Règle activée : alignés {?X ?Y ?Z}
Étape #1 sur 1 : prouve_et_réf EX droite ?d : est_sur ?X ?d ET (est_sur ?Y ?d ET est_sur ?Z ?d)
But(2préf) : EX droite ?d : est_sur A ?d ET (est_sur F ?d ET est_sur D ?d)
Valeurs possibles de ?d : {d1 d2}

But(2préf) (Cas #1 sur 2) : droite d1
But(3.1) : est_sur A d1 ET (est_sur F d1 ET est_sur D d1)
But(4a) : est_sur A d1
Règle activée : NON est_sur ?P ?d
Étape #1 sur 1 : prouve VRAI
But(5réf) : VRAI
But(5réf) : VRAI : VRAI
But(4a) : est_sur A d1 : FAUX
But(3.1) : est_sur A d1 ET (est_sur F d1 ET est_sur D d1) : FAUX

But(2préf) (Cas #2 sur 2) : droite d2
But(3.2) : est_sur A d2 ET (est_sur F d2 ET est_sur D d2)
But(4a) : est_sur A d2
But(4a) : est_sur A d2 : VRAI
But(4b) : est_sur F d2 ET est_sur D d2
But(5a) : est_sur F d2
But(5a) : est_sur F d2 : VRAI
But(5b) : est_sur D d2
Règle activée : NON est_sur ?P ?d
Étape #1 sur 1 : prouve VRAI
But(6réf) : VRAI
But(6réf) : VRAI : VRAI
But(5b) : est_sur D d2 : FAUX
But(4b) : est_sur F d2 ET est_sur D d2 : FAUX
But(3.2) : est_sur A d2 ET (est_ sur F d2 ET est_sur D d2) : FAUX

But(2préf) : EX droite ?d : est_sur A ?d ET (est_sur F ?d ET est_sur D ?d) : FAUX
But(1) : alignés {A F D} : FAUX

62On voit apparaître ici dans les traces la possibilité d’un suffixe accompagnant le numéro d’un but. Celui-ci permet de garder la trace de la relation entre un but et le but précédent. Il y a principalement quatre possibilités :

• But(5) : Ce but sert à prouver. S’il est VRAI, le But(4) est VRAI.
• But(5réf) : Ce but sert à réfuter. S’il est VRAI, le But(4) est FAUX.
• But(5préf) : Ce but sert à la fois à prouver et à réfuter. S’il est VRAI, le But(4) est VRAI. S’il est FAUX, le But(4) est FAUX.
• But(5nég) : Ce but sert à prouver ou à réfuter la négation du but précédent. S’il est VRAI, le But(4) est FAUX. S’il est FAUX, le But(4) est VRAI.

Analyse

• Le fait d’attendre la réfutation pour introduire le modus ponens est un choix didactique. D’une part, il n’est pas nécessaire de le mentionner pour introduire le moteur d’inférence, ce qui implique déjà d’aborder en même temps plusieurs éléments de connaissance. D’autre part, son apparition dans le contexte de la réfutation permet d’éclaircir une situation possiblement confuse, et par le fait même, de le rendre plus prégnant.
• Le dernier exemple permet de mettre en évidence tout le travail sur le statut des énoncés qui apparaît dans ce contexte. Un énoncé est soit « à prouver », soit « évalué ».

63L’énoncé « à prouver ». — Si c’est un énoncé simple ou la négation d’un énoncé simple, il sert à déclencher des règles. Si c’est un énoncé avec quantificateur, il faut trouver l’ensemble de définition et continuer l’évaluation à partir des éléments de cet ensemble. Si c’est un énoncé composé, il faut évaluer séparément chacune de ses parties.

64L’énoncé « évalué ». — S’il a été généré par l’application d’une règle, sa valeur VRAI ou FAUX peut avoir ou ne pas avoir d’effet selon qu’il s’agit d’une étape pour prouver ou pour réfuter, ou les deux. Si cette valeur ne permet pas de conclure ou est inconnue, il y a possibilité d’activation d’une autre étape ou d’une autre règle. Si l’énoncé fait partie d’un énoncé avec quantificateur ou composé, son effet dépend de la nature du quantificateur ou du connecteur.

65Le moteur est conçu de façon à exploiter toutes les contraintes permettant de rendre son fonctionnement le plus efficace possible. Ainsi, à chaque niveau, il « sait » si seule une réponse VRAI, ou seule une réponse FAUX, ou les deux réponses ont un effet. Si par exemple seule une réponse VRAI a un effet, il ne déclenchera pas les règles servant à réfuter, il n’évaluera pas le second énoncé d’un énoncé avec ET si le premier est de valeur inconnue. Dans ces cas, il va afficher dans les traces complètes les messages « Étape inutile » ou « Inutile de continuer ». Ce sont là autant d’occasions pour l’étudiant de faire fonctionner ses connaissances des mécanismes logiques en jeu pour comprendre ce qui justifie tel fonctionnement dans telle situation.

66E3 : On s’intéresse à étendre à d’autres objets géométriques — segments, triangles, angles, carrés... — les raisonnements qu’on peut programmer avec RAISON. Ceci permet d’introduire le chaînage avant.

67Comment représenter un segment dans la banque d’énoncés ? On peut utiliser le prédicat « segment » pour le nommer, puis utiliser un autre prédicat pour nommer ses extrémités, par exemple :

segment AB
extrémités AB {A B)

68Mais à l’usage, on réalise que seul le second type d’énoncé est vraiment utile. Il est donc plus simple et plus clair de ne conserver que :

segment AB {A B}

69Qu’en est-il dans le cas du triangle ? Comme un triangle est défini par ses sommets, on peut utiliser le prédicat « triangle » avec comme objets un nom et un ensemble de trois points, par exemple :

triangle t [A B C}

70Mais un triangle comprend davantage que ses trois sommets. Les raisonnements sur un triangle peuvent faire intervenir ses côtés, ses angles... On a besoin de nommer ces éléments. Donc un seul triangle va donner lieu à plusieurs énoncés dans la banque, par exemple :

71Le chaînage avant fournit un mécanisme permettant de générer tous ces énoncés en ne tapant que le premier. Il correspond à une seconde interprétation de l’utilisation dans un raisonnement d’un énoncé de la forme « p implique q ». Nous avons vu que l’interprétation associée au chaînage arrière est : si tu veux prouver « q », essaie de prouver « p ». Cette fois l’interprétation est : si tu acceptes « p », accepte aussi « q ».

72On voit que la construction de la représentation d’un triangle donne lieu à ce type d’interprétation de toute une série d’implications :

Si t est un triangle de sommets A, B, C, alors il y a un segment d’extrémités A et B.

Si t est un triangle de sommets A, B, C, alors le segment AB est un côté de t.

Si t est un triangle de sommets A, B, C, alors il y a un angle de sommet A dont les côtés passent respectivement par B et par C.

…

73On crée une règle de chaînage avant en tapant par exemple :

Condition : triangle Pnom {?X ?Y ?Z}
Action : énonce segment ?X & ?Y {?X ?Y}
énonce segment ?X & ?Z {?X ?Z}
énonce segment ?Y & ?Z {?Y ?Z}
énonce côtés ?nom {?X & ?Y ?X & ?Z ?Y & ?Z}
énonce angle ?X {?Y ?Z}
énonce angle ?Y {?X ?Z}
énonce angle ?Z {?X ?Y}

74L’opérateur « & », de concaténation, permet de créer les noms « AB », « BC »...

75Chaque fois qu’un énoncé est introduit dans la banque par l’exécution de l’action « énonce », RAISON commence par ajouter l’énoncé dans la banque, puis effectue un pairage entre cet énoncé et l’énoncé de condition de chacune des règles de chaînage avant. Chaque fois que le pairage réussit, les actions de la règle sont exécutées. Donc en énonçant « triangle t {A B C} », on introduit automatiquement tous les autres énoncés.

76La suite de la séquence consiste à résoudre les problèmes :

771. a) Définissez une règle avant permettant de créer un carré.

78b) Définissez la règle arrière « congrus » permettant d’obtenir :

Énonce >> carré c {A B C D}
Énonce >> triangle t {C D E}
Énonce >> équilatéral t

Prouve >> congrus AB DE
VRAI

792. Programmez sous forme de règle arrière l’axiome CAC de congruence des triangles.

Deux triangles sont congrus s’ils ont en commun deux côtés et l’angle compris entre ces côtés.

80Vérifiez le fonctionnement de votre règle en introduisant deux triangles appropriés et en demandant à RAISON de prouver leur congruence, par exemple :

81Aide. — Il faut se rappeler que la congruence entre triangles est définie en fonction d’une certaine correspondance entre les points. Elle dépend de l’ordre des points. La règle « congrus » doit donc générer un processus de recherche à travers tous les ordres possibles des points. Le quantificateur EX est l’outil permettant de programmer une telle recherche.

82Le logiciel permet d’utiliser EX avec AP (appartient) pour effectuer une recherche sur plusieurs variables en même temps. Par exemple,

EX ?u ?v ?w AP {A B C} : ...

83va générer successivement chacune des six associations possibles où ?u – ?v – ?w soit :

843. Soit le triangle ABC isocèle en A.

85Programmez RAISON pour qu’il prouve que les angles B et C sont congrus.

86Aide. — On peut prouver ce théorème simplement en invoquant la règle CAC. Cette démonstration un peu surprenante a été « découverte » par un ordinateur dans les années soixante. Vous avez ici l’occasion de la reproduire. (Malheureusement pour le programmeur triomphant, on a ensuite réalisé que cette preuve apparaît dans les travaux de Proclus, I^er siècle après J.C. !)

87Cette solution implique d’ajouter trois étapes à la règle « congrus » déjà définie :

• Tout objet est congru à lui-même.
• Deux segments sont congrus s’ils forment deux côtés d’un triangle isocèle en P, qui contiennent chacun le point P.
• Deux angles sont congrus s’ils sont les angles correspondants de deux triangles congrus.

Analyse

• Au début de cette recherche, les notions informatiques de moteur d’inférence et de chaînage avant et arrière étaient conçues comme des outils permettant de contextualiser les savoirs de référence qui étaient vus comme appartenant au champ de la logique. Il me semble maintenant que ces notions méritent d’apparaître comme telles dans les savoirs à enseigner. Ceci implique d’accepter d’inclure dans les mathématiques scolaires des concepts informatiques, tout comme on accepte plus ou moins explicitement d’y inclure des éléments provenant de la psychologie cognitive. En d’autres termes, les mathématiques ne constituent pas le seul savoir savant de référence pour les mathématiques scolaires. Ces considérations posent la question de l’institutionnalisation sous un autre angle. Mais elles n’éliminent pas la question de la viabilité des connaissances développées à l’aide d’un outil informatique dans un contexte non informatique.
• Les trois problèmes présentés constituent des activités de synthèse pour tout ce qui a été introduit jusqu’à présent. D’après mon expérience, ce sont des problèmes difficiles qui demandent qu’on donne aux étudiants le temps et l’encadrement appropriés. Du point de vue de la géométrie, ce sont des problèmes très élémentaires. On voit que RAISON est un micromonde de logique, et que ce logiciel peut difficilement prétendre contribuer de façon significative à l’apprentissage des concepts de la géométrie.

Règles logiques et principes de démonstration

88E1 : On passe maintenant à des raisonnements sur les nombres. RAISON permet d’utiliser les prédicats =, <, >, ≤ et ≥. Il accepte également les opérations numériques (op) +,*, /, \ (reste de la division) et ^ (puissance). On peut par exemple programmer des règles permettant de décider si un entier est pair ou impair :

But : pair ?n
Étape : prouve_et_réf ?n\2 = 0

But : impair ?n
Étape : prouve_et_réf NON pair ?n

89Ce type de raisonnement se réduit essentiellement à effectuer des calculs. La situation devient plus intéressante si on essaie de prouver des énoncés concernant tous les entiers ou, ce qui revient au même, concernant un entier quelconque qu’on identifie par une lettre.

90On peut donc formuler des énoncés tel :

Prouve >> pair 2 * n

91On a alors l’occasion de formuler des règles telles :

• Le produit de deux entiers est pair si et seulement si au moins un des deux est pair.
• La somme ou la différence de deux entiers est paire si et seulement si les deux nombres sont pairs ou les deux nombres sont impairs.
• Le quotient de deux entiers est pair si et seulement si...

92Le logiciel permet d’utiliser un prédicat avec un nombre variable d’objets, d’où les règles :

But : pair ?x *?y
Étape : prouve_et_réf pair ?x OU pair ?y

But : pair ?x + ?y
Étape : prouve_et_réf (pair ?x ET pair ?y) OU (impair ?x ET impair ?y)

But : impair ?x ?op ?y
Étape : prouve_et_réf NON pair ?x ?op ?y

93Ces règles ne peuvent être déclenchées que si le prédicat est accompagné de trois objets. RAISON permet de délimiter un objet en utilisant les parenthèses, d’où :

Prouve >> pair 2 * n
VRAI
Prouve >> pair 6 * n * k
Valeur inconnue.
Prouve >> pair (6 * n) * k
VRAI
Prouve >> pair 6 * (n * k)
VRAI
Prouve >> pair (2 * n) + 1
FAUX

94Voici une version abrégée de la dernière démonstration :

But(1) : pair (2 * n) + 1
Règle activée : pair ?x + ?y
Étape #1 sur 1 : prouve_et_réf (pair ?x ET pair ?y) OU (impair ?x ET impair ?y)
But(2préf) : (pair (2 * n) ET pair 1) OU (impair (2 * n) ET impair 1)
But(3a) : pair (2 * n) ET pair 1
But(4a) : pair 2 * n
Règle activée : pair ?x * ?y
Étape #1 sur 1 : prouve_et_réf pair ?x OU pair ?y
But(5préf) : pair 2 OU pair n

95…

But(5préf) : pair 2 OU pair n : VRAI
But(4a) : pair 2 * n : VRAI
But(4b) : pair 1

96…

But(4b) : pair 1 : FAUX
But(3a) : pair (2 * n) ET pair 1 : FAUX
But(3b) : impair (2 * n) ET impair 1
But(4a) : impair 2 * n
Règle activée : impair ?x ?op ?y
Étape #1 sur 1 : prouve_et_réf NON pair ?x ?op ?y
But(5préf) : NON pair 2 * n
But(5préf) : NON pair 2 * n : FAUX
But(4a) : impair 2 * n : FAUX
But(3b) : impair (2 * n) ET impair 1 : FAUX
But(2préf) : (pair (2 * n) ET pair 1) OU (impair (2 * n) ET impair 1) : FAUX
But(1) : pair (2 * n) + 1 : FAUX

97Considérons maintenant :

Prouve >> pair 3 * n
Valeur inconnue

98Comme la réponse dépend de la parité de n, le moteur ne trouve pas de valeur. On pourrait ici vouloir prouver « 3 * n » sous l’hypothèse « pair n » ou « impair n ». Une façon de procéder consisterait à ajouter puis à enlever successivement chacune des hypothèses. L’action « prouve_hyp » permet d’éviter ces manipulations :

Prouve_hyp >> pair 3 * n | pair n
VRAI

99Mais ceci ne fonctionne pas pour l’autre hypothèse. Pourquoi ?

Prouve_hyp >> pair 3 * n | impair n
Valeur inconnue

100En examinant les traces, on constate que le moteur n’arrive pas à déduire que « pair n » est FAUX si « impair n » est VRAI. C’est compréhensible puisqu’aucune règle ne lui permet de le faire. En fait, on peut introduire ces deux énoncés dans la banque :

Énonce >> pair n
Énonce >> impair n

101sans que RAISON ne réagisse ! Mais, si on ajoute :

Énonce >> NON pair n

102on obtient le message « CONTRADICTION » et il refuse d’introduire cet énoncé dans la banque.

103Pour lui enseigner à raisonner en tenant compte du fait que « impair » est la négation de « pair », on définit la règle de chaînage avant :

Condition : impair ?n
Action : énonce NON pair ?n

104On obtient alors :

But(1hyp): pair 3 * n | impair n
Supposons : impair n : VRAI
** AJOUT : impair n
** AJOUT : NON pair n
But(2préf) : pair 3 * n
Règle activée : pair ?x * ?y
Étape #1 sur 1 : prouve_et_réf pair ?x OU pair ?y
But(3préf) : pair 3 OU pair n
But(4a) : pair 3
Règle activée : pair ?n
Étape #1 sur 1 : prouve_et_réf ?n \ 2 = 0
But(5préf) : 3 \ 2 = 0
But(5préf) : 3 \ 2 = 0 : FAUX
** AJOUT : NON pair 3
But(4a) : pair 3 : FAUX
But(4b) : pair n
But(4b) : pair n : FAUX
But(3préf) : pair 3 OU pair n : FAUX
** AJOUT : NON pair 3 * n
But(2préf) : pair 3 * n : FAUX
But(1 hyp) : pair 3 * n | impair n : FAUX
** RETRAIT : impair n
** RETRAIT : NON pair n
** RETRAIT : NON pair 3
** RETRAIT : NON pair 3 * n

105Accepter l’hypothèse « impair n », c’est l’introduire dans la banque. La règle avant est alors activée, ce qui introduit également « NON pair n ». Aussi l’énoncé « pair n » est immédiatement évalué « FAUX », sans que le moteur n’ait besoin d’activer une règle.

106Il est intéressant ici de se demander ce que le moteur va répondre si on lui demande de prouver un énoncé en acceptant simultanément deux hypothèses contradictoires, et pourquoi il est programmé ainsi :

But(1 hyp) : n’importe quoi | pair n, impair n
Supposons : pair n : VRAI
Supposons : impair n : VRAI
Contradiction !
n’importe quoi : VRAI
But(1hyp) : n’importe quoi | pair n, impair n : VRAI

107On sait que le produit de deux entiers consécutifs est pair. Est-ce que les règles introduites jusqu’à présent permettent de le prouver ? Il se trouve que oui, mais en utilisant une propriété du moteur qui n’a pas encore été introduite. Voici les traces abrégées de cette démonstration :

But(1) : pair n * (n + 1)
Règle activée : pair ?x * ?y
Étape #1 sur 1 : prouve_et_réf pair ?x OU pair ?y
But(2préf) : pair n OU pair (n + 1)
Règle logique : (e1 OU e2) équivalent à (NON e1 >> e2)
But(3hyp) : pair (n + 1) | NON pair n
Supposons : NON pair n : VRAI
But(4préf) : pair n + 1
Règle activée : pair ?x + ?y
Étape #1 sur 1 : prouve_et_réf (pair ?x ET pair ?y) OU (impair ?x ET impair ?y)
But(5préf) : (pair n ET pair 1) OU (impair n ET impair 1)
But(6b) : impair n ET impair 1
But(7a) : impair n
Règle activée : impair ?n
Étape #1 sur 1 : prouve_et_réf NON pair ?n
But(8préf) : NON pair n
But(8préf) : NON pair n : VRAI
But(7a) : impair n : VRAI
But(7b) : impair 1
But(7b) : impair 1 : VRAI
But(6b) : impair n ET impair 1 : VRAI
But(5préf) : (pair n ET pair 1) OU (impair n ET impair 1) : VRAI
But(4préf) : pair n + 1 : VRAI
But(3hyp) : pair (n + 1) | NON pair n : VRAI
But(2préf) : pair n OU pair (n + 1) : VRAI
But(1) : pair n * (n + 1) : VRAI

108Le logiciel contient un certain nombre de règles logiques préprogrammées. Celle utilisée ici pose que les énoncés de la forme « e1 OU e2 » et « NON el » e2 » sont équivalents. Cela signifie en particulier que si on réussit à prouver le second, on accepte par cette règle le premier. C’est ce qui se passe dans cet exemple. Le moteur échoue à trouver une valeur séparément pour « pair n » et « pair n+1 ». Dans ce cas, il active automatiquement la règle logique qui lui permet de poser que « pair n OU pair n+1 » est équivalent à « NON pair n » pair n+1 ». Il essaie ensuite de prouver ce dernier énoncé en prouvant « pair n+1 » sous l’hypothèse « NON pair n ». Comme cette voie réussit, il peut accepter « pair n OU pair n+1 ».

109Deux énoncés sont logiquement équivalents s’ils ont la même table de vérité, ou en d’autres mots, si le fait de les relier par une double implication donne une table de vérité qui ne contient que des « VRAI », ce qu’on appelle aussi une tautologie. C’est ce qu’on constate ici :

110On peut comprendre intuitivement que si « NON el » e2 » est VRAI, « el OU e2 » doit nécessairement être VRAI en se disant :

• « pair n » est soit VRAI, soit FAUX.
• S’il est VRAI, alors « pair n OU pair n+1 » est également VRAI.
• S’il est FAUX et si on peut montrer que cela implique que « pair n+1 » est VRAI, alors on a encore « pair n OU pair n+1 » VRAI.
• Donc « pair n OU pair n+1 » est toujours VRAI !

111Curieusement à première vue, après qu’on ait ajouté la règle pour « ^ », le moteur ne réussit pas à prouver une autre forme du même énoncé :

Prouve » pair (n^2) + n

Valeur inconnue

112La raison en est que la règle logique n’est d’aucun secours dans ce cas puisque aucun des énoncés « NON pair (n^2) » pair n » et « NON pair n » pair n^2 » n’est VRAI. Mais on peut quand même retrouver d’une autre façon ce principe d’une preuve par décomposition, à savoir que si un énoncé au sujet de n est VRAI que n soit pair ou impair, alors il est toujours VRAI. Effectivement, on obtient :

Prouve_hyp >> pair (n^2) + n | pair n
VRAI
Prouve_hyp >> pair (n^2) + n | impair n
VRAI

113On peut l’obtenir directement en utilisant l’action « prouve_chaque_hyp » qui essaie de prouver l’énoncé donné mais en acceptant successivement chaque hypothèse :

Prouve_chaque_hyp >> pair (n^2) + n | pair n, impair n
VRAI

Analyse

• Au cours des diverses étapes de ce projet, la question s’est souvent posée de savoir s’il serait intéressant d’intégrer au logiciel certaines connaissances en géométrie, ou sur les nombres, ou sur le calcul algébrique. Pour conserver l’emphase sur les mécanismes logiques du raisonnement, j’ai choisi de ne rien inclure en géométrie. La question me semble différente dans le cas des nombres, car les prédicats et opérations implantées rendent facilement disponibles des raisonnements numériques simples qui ne seraient pas vraiment abordables autrement. Pour ce qui est du calcul algébrique, la question reste ouverte à ce stade-ci. Les raisonnements généraux sur les nombres sont facilités par une implantation très particulière des prédicats « = » et « – ». Ceux-ci produisent normalement soit VRAI, soit FAUX. Cependant si un de leurs objets contient un nombre ou un symbole d’opération numérique, sans être une expression arithmétique, la réponse est « valeur inconnue ».
• Une des caractéristiques intéressantes des raisonnements sur les nombres est l’omniprésence de la double implication. J’ai observé que simplement clarifier toutes les possibilités de « pair » et « impair » avec des nombres n’est pas particulièrement évident. Les raisonnements avec des paramètres, en plus d’introduire implicitement le principe de généralisation, donnent lieu à une familiarisation avec la structure des raisonnements impliquant la coordination des OU et des ET.
• La notion de contradiction est inscrite dans le logiciel à deux niveaux. D’abord, il n’accepte pas d’inclure dans la banque la négation d’un énoncé qui s’y trouve déjà. Mais comme on l’a vu avec pair-impair, l’utilisateur doit gérer les cas où un prédicat réfère à la négation d’un autre. De plus, si on demande au moteur de prouver un énoncé sous une hypothèse correspondant à la négation d’un énoncé de la banque, il répond VRAI. Comprendre ce phénomène donne lieu à une réflexion sur le fonctionnement de l’implication, et possiblement à une prise de conscience de la raison pour laquelle les mathématiciens sont si allergiques aux contradictions !
• L’élément central de toute cette section est la notion de règle logique en tant que fondement des différents principes de démonstration. La notion de preuve sous hypothèses, qui a été introduite comme une façon rapide d’ajouter et d’enlever des énoncés dans la banque, va s’avérer être, comme on a commencé à le voir, un support important pour une meilleure compréhension du fonctionnement de l’implication dans un raisonnement. La notion de règle logique a été introduite en référant à la table de vérité d’une tautologie, mais aussi comme une relation qu’on peut comprendre « intuitivement » par un certain raisonnement. La notion de principe de démonstration, qui avait été introduite avec le modus ponens, réapparaît avec la preuve par décomposition. L’épisode suivant va faire la relation entre ces trois notions.

114E2 : Nous avons vu jusqu’à présent que le chaînage avant et le chaînage arrière constituent deux façons d’utiliser une implication, soit un énoncé de la forme « p >> q », dans un raisonnement. Ce sont là deux utilisations du principe de démonstration appelé modus ponens. Nous allons maintenant examiner comment on peut non pas utiliser une implication déjà prouvée ou acceptée, mais en prouver une nouvelle.

115Pour prouver « p >> q », on peut évaluer séparément « p » et « q ». Si on obtient les deux valeurs, la table de vérité permet de déterminer la valeur de « p >> q », qui est VRAI sauf lorsque « p » est VRAI et « q » FAUX. C’est pourquoi d’ailleurs, dans certains cas (« p » FAUX ou bien « q » VRAI), une seule des deux valeurs permet de conclure. Mais si l’évaluation séparée de « p » et de « q » ne permet pas de conclure, que peut-on faire ? On peut accepter « p » et essayer de prouver « q ». Si cela réussit, on accepte « p >> q ». Dans les termes du logiciel, on utilise la règle :

But : ?p >> ?q
Étape : prouve _hyp ?q | ?p

116Pourquoi ce principe de démonstration fonctionne-t-il ? Pour s’en convaincre, il suffit d’examiner les différentes possibilités de la table de vérité de l’implication. On ne connaît pas la valeur de « p », mais on sait qu’elle est soit VRAI, soit FAUX. Si elle est VRAI, comme on a prouvé que « q » est VRAI si « p » est VRAI, on a donc nécessairement « p >> q » VRAI. Et si elle est FAUX, on a « p >> q » VRAI quelle que soit la valeur de « q ». Donc, dans les deux cas possibles, « p >> q » est VRAI.

117Mais on peut se demander ce qu’il faut faire si « q | p » est FAUX. On veut prouver « p >> q ». On accepte « p ». On essaie de prouver « q » et on obtient FAUX. Que peut-on conclure ?

118Si on reprend le raisonnement précédent, on réalise qu’on a trouvé que si « p » est VRAI, « q » est FAUX. Ceci pourrait nous amener à conclure que « p » q » est FAUX. Mais il faut se rappeler qu’on ne sait pas si « p » est VRAI ou FAUX ! Si « p » est FAUX, « p >> q » est VRAI. Donc les deux possibilités ne concordent pas et on ne peut rien conclure. C’est pourquoi, dans la règle, nous avons utilisé « prouve_hyp » et non « prouve_hyp_et_ réf ». En réalité, si en acceptant « p », on obtient « NON q », on se trouve à prouver l’énoncé « p » NON q ».

119Voilà pourquoi RAISON se comporte de la façon suivante :

prouve >> pair n+2 | impair n
FAUX
prouve >> impair n >> pair n + 2
Valeur inconnue

prouve >> impair n » NON pair n + 2
VRAI

120Partant d’une banque qui ne contient ni « p », ni « q », voici la trace de « p >> q » :

But(1) : p >> q
But(2a) : p
But(2a) : p : Valeur inconnue
But(2b) : q
But(2b) : q : Valeur inconnue
Principe de démonstration : Pour prouver e1 >> e2, prouver e2 | e1
But(2hyp) : q | p
Supposons : p : VRAI
But(3préf) : q
But(3préf) : q : Valeur inconnue
But(2hyp) : q | p : Valeur inconnue
Règle logique : (e1 >> e2) équivalent à (NON e2 >> NON e1)
But(2hyp) : NON p | NON q
Supposons : NON q : VRAI
But(3préf) : NON p
But(3préf) : NON p : Valeur inconnue
But(2hyp) : NON p | NON q : Valeur inconnue
But(1) : p » q : Valeur inconnue

121On voit que le moteur commence par évaluer séparément « p » et « q ». Comme il n’est pas capable de conclure, il essaie « q | p », selon le principe de démonstration qui consiste à transformer une implication en énoncé sous hypothèse. Comme il n’est pas encore capable de conclure, il essaie « NON p | NON q ». Cette dernière tentative est justifiée par la règle logique (p >> q) <<>> (NON q >> NON p). On peut vérifier qu’il s’agit bien d’une règle logique en utilisant les tables de vérité. Et comme, par cette équivalence logique, on peut remplacer l’implication de départ par une autre implication, on peut encore utiliser, avec cette seconde implication, notre principe de démonstration.

122On peut constater une démarche semblable dans l’évaluation des énoncés composés avec les connecteurs ET et OU. On en a vu un exemple avec OU dans l’épisode précédent. L’idée générale est que s’il existe une règle logique permettant de transformer un énoncé composé en implication, on peut utiliser le principe de démonstration qui permet de le transformer en énoncé sous hypothèse.

123Les connecteurs ET et OU donnent lieu aux règles logiques :

(p OU q) <<>> (NON p >> q) <<>> (NON q >> p)
NON (p ET q) <<>> (p >> NON q) <<>> (q >> NON p)

124ce qui correspond dans le logiciel aux règles préprogrammées :

But : ?p OU ?q
Étape : prouve_hyp ?q | NON ?p
prouve_hyp ?p | NON ?q

But : p ET q
Étape : prouve_hyp_réf NON ?q | ?p
prouve_hyp_réf NON ?p | ?q

125Une règle logique (ou tautologie) est un énoncé composé dont la valeur est VRAI, quelles que soient les valeurs des énoncés qui le composent. Une contradiction est un énoncé composé dont la valeur est FAUX, quelles que soient les valeurs des énoncés qui le composent. Dans le contexte de RAISON, on a une règle logique (ou une contradiction) si on obtient VRAI (ou FAUX) comme évaluation d’un énoncé composé dont les énoncés qui le composent sont de valeur inconnue. Par exemple :

But(1) : p OU NON p
Règle logique : (e1 OU e2) équivalent à (NON e1 >> e2)
But(2hyp) : NON p | NON p
Supposons : NON p : VRAI
But(3préf) : NON p
But(3préf) : NON p : VRAI
But(2hyp) : NON p | NON p : VRAI
But(1) : p OU NON p : VRAI
But(1) : p ET NON p
Règle logique : NON (e1 ET e2) équivalent à (e1 >> NON e2)
But(2hyp_réf) : NON NON p | p
Supposons : p : VRAI
But(3préf) : p
But(3préf) : p : VRAI
But(2hyp_réf) : NON NON p | p : VRAI
But(1) : p ET NON p : FAUX

126Ainsi les règles logiques préprogrammées servent à prouver d’autres règles logiques. En plus de celles mentionnées jusqu’à présent, le logiciel inclut des règles préprogrammées permettant de traiter les connecteurs <<>> et OUX, la négation de conjonctions et de disjonctions, ainsi que les situations où on a à accepter un énoncé composé comme hypothèse.

127La suite de la séquence consiste à examiner des règles logiques qui ont une signification particulière dans le contexte de la démonstration.

128Ainsi « NON (p et NON p) » correspond au principe de non contradiction, à savoir qu’un énoncé et sa négation ne peuvent pas être VRAI tous les deux en même temps. On a vu que ce principe est inscrit dans le mécanisme d’entrée des énoncés dans la banque, et que si on l’ignore, on peut prouver n’importe quoi.

129« p OU NON p » correspond au principe du tiers exclu. Un énoncé est soit VRAI, soit FAUX. Il n’y a pas d’autre possibilité. (Une formulation plus exacte de ce principe serait « p OUX NON p », qui est aussi une tautologie.) On a utilisé implicitement ce principe pour justifier la preuve par décomposition.

130Ce principe de démonstration par décomposition peut être formulé comme une règle logique. En voici la démonstration :

But(1) : ((p >> r) ET (NON p >> r)) >> r
Principe de démonstration : Pour prouver e1 >> e2, prouver e2 | e1.
Règle logique : (e1 >> e2) équivalent à (NON e2 >> NON e1)
But(2hyp) : NON ((p >> r) ET (NON p >> r)) | NON r
Supposons : NON r : VRAI
But(3préf) : NON ((p >> r) ET (NON p >> r))
Règle logique : NON (e1 ET e2) équivalent à (NON e1) OU (NON e2)
But(4préf) : NON (p >> r) OU NON (NON p >> r)
Règle logique : (e1 OU e2) équivalent à (NON e1 >> e2)
But(5hyp) : NON (NON p » r) | NON NON (p >> r)
Supposons : p >> r : VRAI
Règle logique : (e1 >> e2) équivalent à (NON e1 OU e2)
Soit : NON p OU r : VRAI
Règle logique : (e1 OU e2) >> e3 équivalent à (e1 >> e3) ET (e2 >> e3)
Les deux cas sont nécessaires.
But(6hyp_a) : NON (NON p >> r) | NON p
Supposons : NON p : VRAI
But(7préf) : NON (NON p >> r)
But(8nég) : NON p >> r
But(9b) : r
But(9b) : r : FAUX
But(8nég) : NON p >> r : FAUX
But(7préf) : NON (NON p >> r) : VRAI
But(6hyp_a) : NON (NON p >> r) | NON p : VRAI
But(6hyp_b) : NON (NON p >> r) | r
Supposons : r : VRAI
Contradiction !
NON (NON p >> r) : VRAI
But(6hyp_b) : NON (NON p >> r) | r : VRAI
But(5hyp) : NON (NON p >> r) | NON NON (p >> r) : VRAI
But(4préf) : NON (p >> r) OU NON (NON p >> r) : VRAI
But(3préf) : NON ((p >> r) ET (NON p >> r)) : VRAI
But(2hyp) : NON ((p >> r) ET (NON p >> r)) | NON r : VRAI
But(1) : ((p >> r) ET (NON p >> r)) >> r : VRAI

131Cet exemple fait intervenir des règles préprogrammées associées aux connecteurs >> et OU, à la transformation de la négation d’une conjonction en disjonction de négations, à la transformation d’une implication en disjonction, et à la décomposition en deux cas de l’acceptation d’une disjonction comme hypothèse.

132On peut maintenant passer à des problèmes du type :

1. Est-ce que p >> NON p est une contradiction ? Vérifiez votre réponse à l’aide de RAISON.
2. Si l’énoncé (p >> q) OU (q >> p) est toujours VRAI, cela signifie que du point de vue de la logique il y a toujours un lien d’implication entre deux énoncés, dans un sens ou dans l’autre, quels que soient ces énoncés. Est-ce vrai ?
3. Formulez la règle logique à la base du principe du modus ponens. Prédisez comment RAISON va démontrer cette règle, puis vérifiez votre prédiction.
4. Une démonstration par l’absurde consiste à prouver qu’un énoncé est VRAI en montrant que sa négation conduit à une contradiction. Quelle est la règle logique à la base de ce principe ? Prédisez comment RAISON va démontrer cette règle, puis vérifiez votre prédiction.

Analyse

• On en arrive finalement à un travail sur la logique qui ne fait référence à aucun contenu. Même les concepts de la logique ne sont pas vus comme des contenus en soi mais comme servant à comprendre le mécanisme de la démonstration. C’est pourquoi l’implication joue un rôle central. Tout repose sur deux grands principes. Le modus ponens permet d’utiliser une implication dans le processus de démonstration. Le principe de transformation d’une implication en énoncé sous hypothèse permet de démontrer une implication et, par le biais des règles logiques, tout énoncé composé (qui ne contient pas d’énoncé avec quantificateur). Une nouvelle activité apparaît, la démonstration de règles logiques. Elle permet de mettre en évidence le fondement logique de différents principes de démonstration.
• L’utilisation de l’informatique permet de mettre en évidence des éléments de connaissance concernant la relation entre logique et démonstration qui sont rarement explicités dans l’enseignement. Cette contribution se situe à deux niveaux. Du point de vue conceptuel, les notions de moteur d’inférence, de chaînage avant ou arrière, de pairage... permettent de représenter et d’expliciter le fonctionnement des connaissances logiques à la base de la démonstration. Du point de vue des processus d’apprentissage, l’ordinateur permet effectivement de faire fonctionner ces connaissances aussi bien dans leur représentation informatique que, par les interactions entre le logiciel et l’étudiant. En un sens, le problème avec l’enseignement des mécanismes logiques de la démonstration, ce n’est pas notre incapacité de les décrire. C’est que le seul fait de les décrire n’en favorise pas l’acquisition. La séquence d’activités avec RAISON présentée dans ce texte constitue une proposition de démarche d’enseignement qui théoriquement contourne ce problème.
• Ce logiciel n’aurait pu être conçu par personne d’autre qu’un didacticien. Il est clair que la conception et l’implantation d’un moteur d’inférence seront fort différentes selon qu’on cherche à en faire un outil efficace pour diverses applications pratiques ou un outil d’apprentissage. La didactique doit façonner ses outils à la lumière de ses problématiques propres. Ceci n’exclut pas la possibilité que ces problématiques soient elles-mêmes façonnées par l’apport de l’informatique. C’est là, me semble-t-il, un résultat important de cette recherche. Dans cette optique, il faut accepter le fait que la conception du logiciel soit indissociable de la conception des activités qu’elle permet, et même de l’analyse et de la délimitation du domaine de connaissances visé.