Dans le cadre de ce projet de recherche, nous nous intéressons à ces quatrièmes cours obligatoires de mathématiques que plusieurs cégeps ont inclus dans leur programme de formation pré-universitaire Sciences de la nature 200. BO. Plus précisément, nous allons nous intéresser à la préparation en matière de démonstration et de formalisme offerte par ces cours pour affronter les exigences des mathématiques post-secondaires. Ces cours ont en effet pour objectif de préparer les étudiants aux mathématiques avancées des cours Calcul intégral NYB et Algèbre linéaire et géométrie vectorielle NYC, mais aussi des cours de mathématiques à l'université, notamment au regard du formalisme accru et de la démonstration. Pour évaluer cette préparation, nous allons, dans un premier temps, étudier ces attentes telles qu'elles se manifestent à travers le cours Calcul intégral NYB, deuxième cours de mathématiques obligatoire de la formation standard en sciences de la nature. Une fois ces attentes identifiées, les tâches proposées dans un de ces quatrièmes cours de mathématiques, soit le cours Mathématiques pour les sciences dispensé par le cégep Ahuntsic à la session hiver 2008, seront analysées. L'analyse des tâches proposées par Mathématiques pour les sciences nous permet de mettre en lumière les éléments de difficultés auxquels il confronte les étudiants. En conclusion, les analyses des deux cours sont comparées pour évaluer si les éléments travaillés par Mathématiques pour les sciences correspondent à ceux sollicités en Calcul intégral NYB. Cette comparaison permet d'évaluer la préparation qui est effectivement offerte par le cours du cégep Ahuntsic pour affronter le cours collégial NYB. Notre étude va cependant plus loin puisque nous évaluons également la préparation que ces deux cours de niveau collégial offrent pour affronter les mathématiques universitaires. Plus précisément, nous tentons de voir, compte tenu de ce que la recherche nous dit des mathématiques avancées et de l'apprentissage de la preuve, si Calcul intégral NYB, appuyé par Mathématiques pour les sciences, constituent à eux deux une bonne transition vers les mathématiques universitaires, notamment les cours d'introduction à l'analyse réelle. Des pistes de réflexion et des améliorations possibles seront également présentées. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : didactique des mathématiques, transition, démonstration, formalisme, calcul intégral

Cette thèse propose et étudie de nouveaux systèmes déductifs mêlant calculs et déductions. La déduction modulo est un premier formalisme qui traduit un pouvoir calculatoire grâce à un système de réécriture. Nous présentons un paradigme dual appelé superdéduction qui traduit un pouvoir déductif par de nouvelles inférences. Ces pouvoirs calculatoires et déductifs modifient la représentation des preuves et leur interaction par les processus d'élimination des coupures. La normalisation forte ou l'admissibilité des coupures ne sont plus garanties et apparaissent alors comme des propriétés intrinsèques des théories représentées sous forme de systèmes de réécriture. Nous démontrons que certains critères permettent d'assurer ces propriétés, notamment en définissant un langage de termes de preuve pour la superdéduction et en étudiant la permutabilité des inférences en calcul des séquents classique. Notre attention est focalisée sur les calculs des séquents classiques et la représentation des preuves dans de tels systèmes. D'autres formalismes connexes sont envisagés, notamment les réseaux de preuve et le focusing. Nous comparons cette dernière approche à la superdéduction, ce qui nous amène à proposer une refonte du paradigme de superdéduction basée sur un système de multifocusing pour la logique classique. Nous en montrons les effets bénéfiques en démontrant la complétude des systèmes déductifs obtenus. / In this thesis we propose and study several deduction systems that mix deduction and computation. Deduction modulo proposes to translate a computational power through a rewriting system. We present the dual concept called superdeduction. It translates a deductive power into custom inference rules that enrich the deduction system. These computational and deductive powers modify the representation of proofs as well as their interaction through cut-elimination processes. Strong normalisation or cut-admissibility may be lost and therefore appear as intrinsic properties of theories represented as rewriting systems. We prove that certain criteria imply these properties by defining a proof-term language for superdeduction and by studying the permutability of inferences in classical sequent calculus. Our attention is focused on classical sequent calculi and on the representation of proofs in such systems. Other related paradigms are considered, namely proof-nets and focusing. We compare this latter approach with superdeduction. We consequently reforge the superdeduction paradigm on top of a multifocusing system for classical logic. We demonstrate the benefits of this approach by proving the completeness of the obtained deduction systems.

Cette thèse propose et étudie de nouveaux systèmes déductifs mêlant calculs et déductions. La déduction modulo est un premier formalisme qui traduit un pouvoir calculatoire grâce à un système de réécriture. Nous présentons un paradigme dual appelé superdéduction qui traduit un pouvoir déductif par de nouvelles inférences. Ces pouvoirs calculatoires et déductifs modifient la représentation des preuves et leur interaction par les processus d'élimination des coupures. La normalisation forte ou l'admissibilité des coupures ne sont plus garanties et apparaissent alors comme des propriétés intrinsèques des théories représentées sous forme de systèmes de réécriture. Nous démontrons que certains critères permeent d'assurer ces propriétés, notamment en définissant un langage de termes de preuve pour la superdéduction et en étudiant la permutabilité des inférences en calcul des séquents classique. Notre attention est focalisée sur les calculs des séquents classiques et la représentation des preuves dans de tels systèmes. D'autres formalismes connexes sont envisagés, notamment les réseaux de preuve et le focusing. Nous comparons cette dernière approe à la superdéduction, ce qui nous amène à proposer une refonte du paradigme de superdéduction basée sur un système de multifocusing pour la logique classique. Nous en montrons les effets bénéfiques en démontrant la complétude des systèmes déductifs obtenus.

Cette thèse s'articule autour de l'utilisation de stratégies totales pour la représentation des preuves. La première partie porte sur le cadre finitaire. L'analyse commence dans un univers syntaxique : on définit un lambda-calcul unaire fortement normalisant, pour lequel on rappelle la machine à pointeurs (PAM). On réduit le problème de préservation de la totalité par composition à un problème de finitude sur des objets appelés structures de pointeurs. On donne trois preuves différentes de ce résultat de finitude. La première se ramène via la PAM à la normalisation du lambda-calcul unaire, la seconde passe par l'extraction d'une réduction simple sur les arbres d'entiers et la troisième s'inspire d'un argument combinatoire de Coquand. La seconde partie traite d'un calcul de séquents mu-LJ équipé de définitions inductives et coinductives, dans lequel on donne une simulation du système T. On définit les catégories mu-fermées, formant une classe de modèles de mu-LJ. Dans le cadre des jeux on définit les arènes ouvertes, munies de variables de type libres. À chacune de ces arènes ouvertes est associé un foncteur ouvert sur la catégorie des stratégies innocentes. On décrit ensuite sur les arènes ouvertes une construction de boucle dont on montre qu'elle rejoint le modèle de McCusker des types récursifs. Les boucles sont alors enrichies par des conditions de gain inspirées des jeux de parité, ce qui équipe les foncteurs ouverts d'algèbres initiales et coalgèbres terminales et construit une catégorie mu-fermée. On propose finalement une extension de mu-LJ à une syntaxe infinie, pour laquelle le modèle est pleinement complet.

Notre recherche s'intéresse aux difficultés que les élèves éprouvent dans l'apprentissage de la preuve au secondaire, notamment celles relatives au changement du statut de la géométrie, lors du passage de la géométrie dite pratique à la géométrie dite théorique. Dans cette optique, nous avons cherché à comprendre comment progressent les exigences de production de la preuve dans les deux premières années du premier cycle du secondaire, à travers les activités géométriques proposées dans les manuels scolaires issus du renouveau pédagogique, en usage dans les deux premières années du secondaire au Québec. Cette interrogation nous a amené à mettre en exergue les orientations qui portent sur l'apprentissage de la preuve dans les nouveaux programmes, à partir de la compétence « Déployer un raisonnement mathématique ». Nous avons ensuite élaboré une grille d'analyse des exercices et problèmes géométriques, sur la base de deux paradigmes géométriques : géométrie I, (GI) et géométrie II, (GII), suggérés par Houdement et Kuzniak dans leurs divers travaux, que nous avons complétée avec la typologie développée par Rouche (1989) et une catégorie de la grille d'analyse de Tanguay (2000). Avec cette grille, nous avons classifié les exercices et problèmes géométriques, spécifiquement en géométrie. De plus, nous avons établi des critères qui nous ont permis d'évaluer l'évolution du statut du dessin, à travers certaines activités classifiées. L'analyse et l'interprétation des résultats de la classification montrent que les exigences de production de preuve ne progressent pas à cause des faibles taux de problèmes qui portent sur la production de la preuve. Aussi, les dessins qui ont un statut d'objet matériel sont dominants dans l'ensemble des deux premières années du secondaire. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Renouveau pédagogique, Preuve, Géométrie pratique, Géométrie théorique.

La production de conjectures, de preuves et de démonstrations mathématiques chez les élèves de l'école secondaire est depuis plusieurs années un thème important de la recherche en didactique des mathématiques. La problématique sous-jacente se complexifie quand on considère de surcroît le rôle que peut jouer la technologie dans l'apprentissage de la preuve et de la démonstration, notamment vis-à-vis la production de conjectures, comme préalable au travail sur une preuve donnée. Ces questions sont ici spécifiées aux élèves de 5e secondaire de l'école québécoise. Le contenu mathématique que nous avons choisi pour étudier ces questions est celui des coniques, approchées avec un logiciel de géométrie dynamique. Plus particulièrement, nous nous sommes intéressés à l'analyse des stratégies et démarches des élèves de 5e secondaire au moment où ils travaillent une démonstration, dans le contexte du thème choisi, d'abord avec papier-crayon et ensuite, avec technologie. Des activités ad hoc ont été élaborées et soumises aux élèves auprès desquels nous avons expérimenté. Les productions qui ont résulté de ces tâches nous ont permis d'analyser les erreurs et obstacles en lien avec la production des conjectures, des preuves et des démonstrations par les élèves. Les résultats issus de l'expérimentation et de l'analyse des productions montrent les aspects positifs et négatifs du travail avec papier-crayon, et aussi de l'environnement technologique. La comparaison de ces deux milieux de travail, des possibilités qu'ils offrent et des contraintes qu'ils sous-tendent pourront servir de piste pour une éventuelle amélioration de l'enseignement des mathématiques à l'école secondaire. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Conjecture, preuve, démonstration, travail papier-crayon, géométrie dynamique, coniques.

De nombreuses recherches ont mis en évidence la difficulté des élèves quant au passage de la géométrie pratique à la géométrie théorique entre l'enseignement primaire et secondaire. Néanmoins, peu de celles-ci se sont penchées sur les solutions à mettre de l'avant afin d'atténuer cette rupture. C'est ce point qui retient notre attention dans le cadre de cette étude. Plusieurs possibilités sont envisageables pour diminuer la rupture entre les deux géométries. Pour notre part, nous avons choisi de nous concentrer sur des activités de géométrie pouvant mener graduellement les élèves de la géométrie pratique à la géométrie déductive. Notre hypothèse étant que les élèves de troisième cycle de l'école primaire sont en mesure de faire de la déduction et d'être initiés à la géométrie théorique. Cette hypothèse est d'ailleurs soutenue par les travaux de Lester (1975) et Douaire (1999). Afin de bien cerner les éléments qui distinguent la géométrie pratique de la géométrie théorique, nous avons fait appel aux travaux de Parzysz (2002) basés sur ceux de van Riele (1984) et de Houdement et Kuzniak (1999). Les outils qu'ils ont développés nous permettent de distinguer plusieurs paradigmes géométriques ainsi que les éléments clés qui les différencient. En nous basant sur ces précédentes études, nous avons mis sur pied une séquence d'activités mettant en lumière les limites de la démarche instrumentée (utilisation de la règle graduée et rapporteur d'angle) tout en souhaitant mettre à profit le développement du raisonnement déductif. Pour la construction de ces activités, nous avons utilisé une démarche de Design Research (Edelson 2002). De plus, nous avons fait appel aux travaux de Coppé et coll. (2005) quant aux différents types de dessin que l'élève rencontre en classe de géométrie. La séquence de neuf activités bâties a été expérimentée dans deux classes de 6e année sur une durée d'environ 4 mois. Les analyses découlant de ces expérimentations ont mis en évidence dans quelle mesure il est possible de favoriser le développement du raisonnement déductif chez les élèves en utilisant des activités d'initiation à la géométrie déductive. De plus, les analyses nous ont aussi permis d'identifier quelles étaient les tâches pouvant mener l'élève à délaisser la mesure au profit de la déduction, tâches qui étaient construites dans l'objectif que l'élève fasse le passage de la géométrie pratique vers la géométrie déductive. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : didactique des mathématiques, raisonnement déductif, paradigmes géométriques, niveaux de van Hiele.

La vérification automatique de preuves consiste à faire vérifier par un ordinateur la validité de démonstrations d'énoncés mathématiques. Cette vérification étant purement calculatoire, elle offre un haut degré de confiance. Elle est donc particulièrement utile pour vérifier qu'un logiciel critique, c'est-à-dire dont le bon fonctionnement a un impact important sur la sécurité ou la vie des personnes, des entreprises ou des biens, correspond exactement à sa spécification. DEDUKTI est l'un de ces vérificateurs de preuves. Il implémente un système de type, le lambda-Pi-Calcul Modulo, qui est une extension du lambda-calcul avec types dépendants avec des règles de réécriture du premier ordre. Suivant la correspondance de Curry-Howard, DEDUKTI implémente à la fois un puissant langage de programmation et un système logique très expressif. Par ailleurs, ce langage est particulièrement bien adapté à l'encodage d'autres systèmes logiques. On peut, par exemple, importer dans DEDUKTI des théorèmes prouvés en utilisant d'autres outils tels que COQ, HOL ou encore ZENON, ouvrant ainsi la voie à l'interopérabilité entre tous ces systèmes. Le lambda-Pi-Calcul Modulo est un langage très expressif. En contrepartie, certaines propriétés fondamentales du système, telles que l'unicité des types ou la stabilité du typage par réduction, ne sont pas garanties dans le cas général et dépendent des règles de réécriture considérées. Or ces propriétés sont nécessaires pour garantir la cohérence des systèmes de preuve utilisés, mais aussi pour prouver la correction et la complétude des algorithmes de vérification de types implémentés par DEDUKTI. Malheureusement, ces propriétés sont indécidables. Dans cette thèse, nous avons donc cherché à concevoir des critères garantissant la stabilité du typage par réduction et l'unicité des types et qui soient décidables, de manière à pouvoir être implémentés par DEDUKTI. Pour cela, nous donnons une nouvelle définition du lambda-Pi-Calcul Modulo qui rend compte de l'aspect itératif de l'ajout des règles de réécriture dans le système en les explicitant dans le contexte. Une étude détaillée de ce nouveau calcul permet de comprendre qu'on peut ramener le problème de la stabilité du typage par réduction et de l'unicité des types à deux propriétés plus simples, qui sont la compatibilité du produit et le bon typage des règles de réécriture. Nous étudions donc ces deux propriétés séparément et en donnons des conditions suffisantes effectives. Ces idées ont été implémentées dans DEDUKTI, permettant d'augmenter grandement sa généralité et sa fiabilité. / Automatic proof checking is about using a computer to check the validity of proofs of mathematical statements. Since this verification is purely computational, it offers a high degree of confidence. Therefore, it is particularly useful for checking that a critical software, i.e., a software that when malfunctioning may result in death or serious injury to people, loss or severe damage to equipment or environmental harm, corresponds to its specification. DEDUKTI is such a proof checker. It implements a type system, the lambda-Pi-Calculus Modulo, that is an extension of the dependently-typed lambda-calculus with first-order rewrite rules. Through the Curry-Howard correspondence, DEDUKTI implements both a powerful programming language and an expressive logical system. Furthermore, this language is particularly well suited for encoding other proof systems. For instance, we can import in DEDUKTI theorems proved using other tools such as COQ, HOL or ZENON, a first step towards creating interoperability between these systems.The lambda-Pi-Calculus Modulo is a very expressive language. On the other hand, some fundamental properties such as subject reduction (i.e., the stability of typing by reduction) and uniqueness of types are not guaranteed in general and depend on the rewrite rules considered. Yet, these properties are necessary for guaranteeing the coherence of the proof system, but also for provingthe soundness and completeness of the type-checking algorithms implemented in DEDUKTI. Unfortunately, these properties are undecidable. In this thesis, we design new criteria for subject reduction and uniqueness of types that are decidable in order to be implemented in DEDUKTI.For this purpose, we give a new definition of the lambda-Pi-Calculus Modulo that takes into account the iterative aspect of the addition of rewrite rules in the typing context. A detailed study of this new system shows that the problems of subject reduction and uniqueness of types can be reduced to two simpler properties that we call product compatibility and well-typedness of rewrite rules.Hence, we study these two properties separately and give effective sufficient conditions for them to hold.These ideas have been implemented in DEDUKTI, increasing its generality and reliability.

En informatique, les logiques formelles ont une place centrale dans la représentation et le traitement des connaissances. Elles sont utilisées pour la modélisation et la vérification de systèmes informatiques et de leurs propriétés ainsi que pour la formalisation de différents types de raisonnement. Dans ce contexte il existe un large spectre de logiques non-classiques parmi lesquelles les logiques modales jouent un rôle important. Alors que les logiques modales classiques ont été largement étudiées, nous nous focalisons dans cette thèse sur les logiques modales intuitionnistes et aussi hybrides floues en abordant un certain nombre de questions principalement du point de vue de la théorie de la démonstration. Nous proposons pour ces logiques de nouveaux systèmes de preuve, notamment suivant les formalismes de déduction naturelle et de calcul des séquents, qui sont fondés sur de nouvelles structures multi-contextuelles généralisant la structure standard de séquent. Ainsi dans le cadre des logiques modales intuitionnistes formées à partir des combinaisons des axiomes T, B, 4 et 5, nous définissons des systèmes de preuve sans labels ayant de bonnes propriétés comme par exemple celle de la sous-formule. En outre, nous proposons des procédures de décision simples à partir de nos nouveaux calculs des séquents. Nous étudions également la première version intuitionniste de la logique hybride IHL et nous proposons son premier calcul des séquents à partir duquel nous donnons la première démonstration de sa décidabilité. Enfin, nous introduisons une nouvelle famille de logiques hybrides floues fondées sur les logiques modales de Gödel. Nous proposons pour ces logiques des procédures de décision avec génération de contre-modèles en utilisant un ensemble de règles de preuve fondées sur une structure multi-contextuelle adaptée.

Cette thèse présente des avancées dans l'utilisation des Structures Canoniques, un mécanisme du langage de programmation de l'assistant de preuve Coq, équivalent à la notion de classes de types. Elle fournit un nouveau modèle pour le développement de hiérarchies mathématiques à l'aide d'enregistrements dépendants, et, en guise d'illustration, fournit une reformulation de la preuve formelle de correction du cryptosystème RSA, offrant des méthodes de raisonnement algébrique ainsi que la représentation en théorie des types des notions mathématiques nécessaires (incluant les groupes cycliques, les groupes d'automorphisme, les isomorphismes de groupe). Nous produisons une extension du mécanisme d'inférence de Structures Canoniques à l'aide de types fantômes, et l'appliquons au traitement de fonctions partielles. Ensuite, nous considérons un traitement générique de plusieurs formes de définitions de sous-groupes rencontrées au long de la preuve du théorème de Feit-Thomspon, une large librairie d'algèbre formelle développée au sein de l'équipe Mathematical Components au laboratoire commun MSR-INRIA. Nous montrons qu'un traitement unifié de ces 16 sous-groupes nous permet de raccourcir la preuve de leur propriétés élémentaires, et d'obtenir des définitions offrant une meilleure compositionnalité. Nous formalisons une correspondance entre l'étude de ces fonctorielles, et des propriété de théorie des groupes usuelles, telles que représentées par la classe des groupes qui les vérifie. Nous concluons en explorant les possibilités d'analyse de la fonctorialité de ces définitions par l'inspection de leur type, et suggérons une voie d'approche vers l'obtention d'instances d'un résultat de paramétricité en Coq.