.

Les règles de transformation des problèmes equationnels sont donnes permettant, en particulier, de décider de l'existence d'une solution fermée. Comme première application, il est montre comment calculer une grammaire pour le langage des termes fermes irréductibles par un système de réécriture. D'autres applications et extensions sont ensuite envisagées. En particulier, en programmation logique et dans les spécifications algébriques

Les schématisations de termes permettent de représenter des ensembles infinis de termes ayant une structure similaire de manière finie et compacte. Dans ce travail, nous étudions certains aspects liés à l'utilisation des schématisations de termes en déduction automatique, plus particulièrement dans les méthodes de démonstration de théorèmes du premier ordre par saturation. Après une brève étude comparée des formalismes de schématisation existants, nous nous concentrons plus particulièrement sur les termes avec exposants entiers (ou I-termes). Dans un premier temps, nous proposons une nouvelle approche permettant de détecter automatiquement des régularités dans les espaces de recherche. Cette détection des régularités peut avoir plusieurs applications, notamment la découverte de lemmes nécessaires à la terminaison dans certaines preuves inductives. Nous présentons DS3, un outil qui implémente ces idées. Nous comparons notre approche avec d'autres techniques de généralisation de termes. Notre approche diffère complètement des techniques existantes car d'une part, elle est complètement indépendante de la procédure de preuve utilisée et d'autre part, elle utilise des techniques de généralisation inductive et non déductives. Nous discutons également les avantages et les inconvénients liés à l'utilisation de notre méthode et donnons des éléments informels de comparaison avec les approches existantes. Nous nous intéressons ensuite aux aspects théoriques de l'utilisation des I-termes en démonstration automatique. Nous démontrons que l'extension aux I-termes du calcul de résolution ordonnée est réfutationnellement complète, que l'extension du calcul de superposition n'est pas réfutationnellement complète et nous proposons une nouvelle règle d'inférence pour restaurer la complétude réfutationnelle. Nous proposons ensuite un algorithme d'indexation (pour une sous-classe) des I-termes, utile pour le traitement des règles de simplification et d'élimination de la redondance. Finalement nous présentons DEI, un démonstrateur automatique de théorèmes capable de gérer directement des formules contenant des I-termes. Nous évaluons les performances de ce logiciel sur un ensemble de benchmarks.

Comment justifier un énoncé en l'absence de tout fondement absolu ? Comment prétendre à la validité dans un contexte de finitude cognitive ?<br /> Après avoir défini les notions de validité et de finitude, ce travail propose la solution suivante.<br /> Au lieu de prétendre à une validité absolue on peut prétendre plus modestement que la position défendue est meilleure que les positions concurrentes connues. On évite ainsi toute ambition absolutiste sans tomber dans le relativisme.<br /> Qu'est-ce qui permet cependant de dire qu'une position est meilleure qu'une autre ? Nous proposons le « critère de préférence » suivant : une position B est meilleure qu'une position A si au moins un problème rencontré par A est résolu par B, et si aucun problème rencontré par B n'est résolu par A.<br /> Lorsque plusieurs positions sont examinées d'après ce critère, l'argumentation prend la forme d'un processus d'apprentissage. En raison de ses similitudes avec la dialectique aristotélicienne, cette procédure est appelée « démonstration dialectique ».<br /> Ce travail examine ensuite la méthodologie de la démonstration dialectique, notamment les règles de recension et de compréhension des positions concurrentes. Il étudie enfin les conséquences de cette procédure sur les concepts épistémologiques tels que la vérité, la connaissance et la rationalité.<br /> Comme la démonstration dialectique est une procédure fondamentale de preuve, elle doit être fondée par elle-même. C'est pourquoi chaque étape de l'argumentation est justifiée à partir d'une confrontation avec les positions concurrentes, notamment celles d'Aristote, Habermas et Popper.

Dans le cadre du présent travail, nous nous intéressons à la transition du secondaire vers le collégial, spécialement en ce qui concerne la démonstration et le formalisme. Nous avons choisi d'évaluer la complexité des tâches de démonstration soumises aux étudiants d'un cours du collégial, Algèbre linéaire et géométrie vectorielle, tel qu'il a été donné au Collège de Maisonneuve à l'hiver 2006, dans le cadre du programme DEC intégré. Nous faisons ensuite une analyse des éléments qui peuvent constituer une préparation à ces tâches, dans le cadre des cours de mathématiques de quatrième et de cinquième secondaires. Par l'analyse de tâches de démonstration de niveau collégial, nous dégageons plusieurs caractéristiques qui contribuent à complexifier largement la production de démonstrations. Nous relevons donc ces caractéristiques et vérifions à travers l'étude des programmes actuels et en processus d'implantation, comment les élèves sont outillés pour faire face à ces éléments de complexité. En conclusion, nous proposons des pistes de réflexions et d'interventions visant à minimiser les impacts de cette transition secondaire-collégial. ______________________________________________________________________________ MOTS-CLÉS DE L’AUTEUR : Didactique des mathématiques, Arrimage secondaire-collégial, Algèbre linéaire, Démonstration, Formalisme.

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.

Cette thèse décrit l'histoire d'un barrage situé dans le sud du Portugal, ayant comme origine un plan d'irrigation des années 50. L'objectif est de comprendre à partir des explications sociologiques et anthropologiques existantes sur les barrages comment l'objet technique noue des liens avec d'autres entités, et comment se composent les chaînes de porte-parole qui font que le projet hydraulique puis plus tard hydroélectrique perdure sans que les abcès de discussions se disséminent. Plusieurs sources d'informations ont composé l'ethnographie multisite du barrage: collecte diachronique de la presse, documents techniques, scientifiques, et audiovisuels, discussions environnementalistes, interventions parlementaires sur l'Alqueva. La presse, ayant constitué notre principal fil conducteur, a permis d'établir un suivi longitudinal exhaustif de la circulation du barrage dans la société. Les pics de cette collecte constituent les sites que nous étudions plus particulièrement. Ces données montrent que la force du barrage se traduit en démonstrations très différentes: par exemple, en 2001 avec la découverte de gravures rupestres et en 2002 avec les inaugurations publiques. C'est également à travers l'histoire du projet d'Alqueva que l'environnement constitue une expérience nouvelle pour divers acteurs. Finalement, le barrage d'Alqueva tient aussi d'un régime d'existence qui précède toutes celles-ci, attaché au plan d'irrigation pour l'Alentejo. Aussi, l'effet du barrage d'Alqueva sur la société portugaise se comprend-t-il comme un effet bien plus qualitatif que cumulatif, son histoire devant être lue comme un mouvement de différentiation progressive et de singularité.

Ce travail est une contribution à la sémantique de jeux des langages de programmation. Il présente plusieurs méthodes nouvelles pour construire une sémantique de jeux pour un lambda-calcul de continuations.Si les sémantiques de jeux ont été développées à grande échelle pour fournir des modèles de langages fonctionnels avec références, en appel par nom et par valeur, ou pour différents fragments de la logique linéaire, certains de ses aspects demeurent cependant très subtils. Cette thèse s'intéresse spécifiquement à la notion d'innocence et à la combinatoire mise en jeu dans la composition des stratégies innocentes, en donnant pour chacune une interprétation via des constructions catégoriques standards.Nous reformulons la notion d'innocence en terme de préfaisceaux booléens sur une catégorie de vues. Pour cela, nous enrichissons la notion de parties dans notre sémantique de jeux en ajoutant des morphismes entre parties qui vont au-delà du simple ordre préfixe habituel. À partir d'une stratégie, donnée par les vues qu'elle accepte, on calcule son comportement sur toutes les parties en prenant une extension de Kan à droite.La composition des stratégies innocentes s'appuie sur les notions catégoriques habituelles de systèmes de factorisation et de foncteurs polynomiaux. Notre sémantique permet de modéliser l'interaction entre deux stratégies comme une seule stratégie dont il faut parvenir à cacher les coups internes, grâce à une technique d'élimination des coupures~: cette étape est accomplie avec une version affaiblie des systèmes de factorisation. La composition elle-même entre stratégies repose pour sa part sur l'utilisation de la théorie des foncteurs polynomiaux. Les propriétés essentielles, telles que l'associativité ou la correction de la sémantique, proviennent d'une méthode de preuve presque systématique donnée par cette théorie. / This work is a contribution to game semantics for programming languages. We describe new methods used to define a game semantics for a lambda-calculus with continuations.Game semantics have been widely used to provide models for functional programming languages with references, using call-by-name or call-by-value, or for different fragments of linear logic. Yet, some parts of these semantics are still highly subtle. This work mainly deals with the notion of innocence, and with combinatorics involved in composing innocent strategies. We provide both of them with an interpretation which relies on standard categorical constructions.We reformulate innocence in terms of boolean presheaves over a given category of views. We design for this purpose an enriched class of plays, by adding morphisms which do not appear in the traditional preorder of plays. We show how to compute the global behaviour, i.e., on every play, of a strategy given by its class of accepted views by taking a right Kan extension.Our composition of innocent strategies relies on the usual categorial notions of factorisation systems and polynomial functors. In our semantics, the interaction between two strategies is itself a strategy, in which we must hide internal moves with a cut-elimination process. This step is given by a weakened version of factorisations systems. The core of composition of strategies involves material borrowed from polynomial functors theory. This theory yields a systematic proof method for showing essential properties, such as associativity of composition, or correction of our semantics.

L'analyse statique des programmes permet d'étudier les comportements possibles des programmes sans les exécuter. Les analyseurs statiques sont employés par exemple pour garantir que l'exécution d'un programme ne peut pas produire d'erreurs. Ces outils d'analyse étant eux-mêmes des programmes, ils peuvent être incorrects. Pour accroître la confiance que l'on peut accorder aux résultats d'une telle analyse, nous étudions dans cette thèse comment on peut formellement établir la correction de l'implantation d'un tel analyseur statique. En particulier, nous construisons au moyen de l'assistant à la preuve Coq des interpréteurs abstraits et prouvons qu'ils sont corrects ; c'est-à-dire nous établissons formellement que le résultat de l'analyse d'un programme caractérise bien toutes les exécutions possibles de ce programme. Ces interpréteurs abstraits s'intègrent, dans la mesure du possible, au compilateur vérifié CompCert, ce qui permet de garantir que les propriétés de sûreté prouvées sur le code source d'un programme sont aussi valides pour la version compilée de ce programme. Nous nous concentrons sur l'analyse de programmes écrits dans des langages de bas niveau. C'est-à-dire des langages qui ne fournissent que peu d'abstractions (variables, fonctions, objets, types…) ou des abstractions que le programmeur a loisir de briser. Cela complexifie la tâche d'un analyseur qui ne peut pas s'appuyer sur ces abstractions pour être précis. Nous présentons notamment comment reconstruire automatiquement le graphe de flot de contrôle de programmes binaires auto-modifiants et comment prouver automatiquement qu'un programme écrit en C (où l'arithmétique de pointeurs est omniprésente) ne peut pas produire d'erreurs à l'exécution. / Static analysis of programs enables to study the possible behaviours of programs without running them. Static analysers may be used to guarantee that the execution of a program cannot result in a run-time error. Such analysis tools are themselves programs: they may have bugs. So as to increase the confidence in the results of an analysis, we study in this thesis how the implementation of static analysers can be formally proved correct. In particular, we build abstract interpreters within the Coq proof assistant and prove them correct. Namely, we formally establish that analysis results characterize all possible executions of the analysed program. Such abstract interpreters are integrated to the formally verified CompCert compiler, when relevant ; this enables to guarantee that safety properties that are proved on source code also hold for the corresponding compiled code. We focus on the analysis of programs written in low-level languages. Namely, languages which feature little or no abstractions (variables, functions, objects, types…) or abstractions that the programmer is allowed to break. This hampers the task of a static analyser which thus cannot rely on these abstractions to yield precise results. We discuss in particular how to automatically recover the control-flow graph of binary self-modifying programs, and how to automatically prove that a program written in C (in which pointer arithmetic is pervasive) cannot produce a run-time error.

Avec la généralisation d'Internet, l'usage des protocoles cryptographiques est devenu omniprésent. Étant donné leur complexité et leur l'aspect critique, une vérification formelle des protocoles cryptographiques est nécessaire.Deux principaux modèles existent pour prouver les protocoles. Le modèle symbolique définit les capacités de l'attaquant comme un ensemble fixe de règles, tandis que le modèle calculatoire interdit seulement a l'attaquant derésoudre certain problèmes difficiles. Le modèle symbolique est très abstrait et permet généralement d'automatiser les preuves, tandis que le modèle calculatoire fournit des garanties plus fortes.Le fossé entre les garanties offertes par ces deux modèles est dû au fait que le modèle symbolique décrit les capacités de l'adversaire alors que le modèle calculatoire décrit ses limitations. En 2012 Bana et Comon ont proposé unnouveau modèle symbolique dans lequel les limitations de l'attaquant sont axiomatisées. De plus, si la sémantique calculatoire des axiomes découle des hypothèses cryptographiques, la sécurité dans ce modèle symbolique fournit desgaranties calculatoires.L'automatisation des preuves dans ce nouveau modèle (et l'élaboration d'axiomes suffisamment généraux pour prouver un grand nombre de protocoles) est une question laissée ouverte par l'article de Bana et Comon. Dans cette thèse nous proposons une procédure de décision efficace pour une large classe d'axiomes. De plus nous avons implémenté cette procédure dans un outil (SCARY). Nos résultats expérimentaux montrent que nos axiomes modélisant la sécurité du chiffrement sont suffisamment généraux pour prouver une large classe de protocoles. / With the rise of the Internet the use of cryptographic protocols became ubiquitous. Considering the criticality and complexity of these protocols, there is an important need of formal verification.In order to obtain formal proofs of cryptographic protocols, two main attacker models exist: the symbolic model and the computational model. The symbolic model defines the attacker capabilities as a fixed set of rules. On the other hand, the computational model describes only the attacker's limitations by stating that it may break some hard problems. While the former is quiteabstract and convenient for automating proofs the later offers much stronger guarantees.There is a gap between the guarantees offered by these two models due to the fact the symbolic model defines what the adversary may do while the computational model describes what it may not do. In 2012 Bana and Comon devised a new symbolic model in which the attacker's limitations are axiomatised. In addition provided that the (computational semantics) of the axioms follows from the cryptographic hypotheses, proving security in this symbolic model yields security in the computational model.The possibility of automating proofs in this model (and finding axioms general enough to prove a large class of protocols) was left open in the original paper. In this thesis we provide with an efficient decision procedure for a general class of axioms. In addition we propose a tool (SCARY) implementing this decision procedure. Experimental results of our tool shows that the axioms we designed for modelling security of encryption are general enough to prove a large class of protocols.