L'étude des moyens de déductions pour entreprendre une construction assistée de programmes mène à la définition d'un système de déduction automatique capable :<br />- de traiter l'égalité d'une façon générale ;<br />- d'entreprendre la preuve de formules qui ne sont pas des théorèmes, d'étudier les causes d'échec ;<br />- d'effectuer un tri pour retirer d'un large ensemble d'informations, celles utiles à la preuve.<br /><br />Ces caractères ont pu être pris en compte dans le cadre d'un système général, de genre "déduction matérielle".<br />Certaines classes d'expression reçoivent toutefois un traitement particulier. Ainsi une méthode de codage permet de déterminer, sans simplification ni mise en forme normale, l'équivalence d'expressions numériques.

Cette thèse, s'intéresse aux systèmes d'interaction, une notion visant à modéliser les interactions entre un système informatique et son environnement.<br /><br />La première partie développe, dans le cadre de la théorie des types de Martin-Löf, la théorie de base des systèmes d'interaction et des constructions inductives et co-inductives qu'ils permettent. On trouve dans cette partie une étude des liens entre systèmes d'interaction et topologies formelles et une formulation (en terme de systèmes d'interaction) d'un théorème de complétude vis-à-vis d'une sémantique topologique des théories géométriques (linéaires).<br /><br />Dans cette étude, la notion complètement standard de simulation, joue un rôle fondamental car elle permet de définir la notion de morphisme entre systèmes d'interaction. Ceci permet d'établir une équivalence entre la catégorie ainsi définie et une autre catégorie, beaucoup plus simple à décrire, celle des transformateurs de prédicats.<br /><br />En traduisant dans ce nouveau vocabulaire les constructions précédentes, on observe que les transformateurs de prédicats forment un nouveau modèle de la logique linéaire, qui est décrit puis étendu au second ordre.<br /><br />Enfin, les propriétés particulières des systèmes d'interaction / transformateurs de prédicats sont mises à profit pour donner une interprétation du lambda-calcul différentiel. Cela suppose d'introduire du non déterminisme, ce que les systèmes d'interaction et les transformateurs de prédicats permettent de faire.

Notre recherche porte sur l'analyse du rôle du langage naturel dans les allers et retours entre domaine théorique et domaine graphique lors d'un processus de démonstration en géométrie plane par des élèves qui travaillent en dyade. Nous nous appuyons en d'abord sur deux hypothèses de recherche : l'une qui considère le langage comme outil d'analyse du discours en tant que révélateur des démarches de résolution, l'autre qui considère le langage comme outil de résolution pour les élèves en tant que médiateur pour la construction et la maîtrise de la pensée. En outre, nous faisons l'hypothèse que l'avancement du processus de résolution passe par l'évolution des échanges verbaux, en se déplaçant d'un mode d'expansion discursive d'accumulation à un mode d'expansion discursive de substitution, et par le changement de la valeur des propositions émises, en passant d'une valeur épistémique à une valeur de vérité. Nous proposons de relever les traces de ces évolutions grâce à l'analyse du discours des binômes observés en retenant l'usage de certaines unités linguistiques comme révélateur d'un type d'expansion discursive. En revanche, pour ce qui concerne l'analyse fonctionnelle du langage en tant qu'outil de résolution, nous retenons l'idée que le langage est outil pour la construction et la maîtrise de la pensée du sujet. Cette perspective nous a permis de dégager les conditions et les modalités d'apparition de diverses fonctions du langage telles la fonction de guide (rôle des verbalisations des théorèmes et de l'instanciation), la fonction de planification (planification d'un enchaînement de pas de déductions), la fonction de contrôle (liée à la fonction de guidage qui permet de revenir sur les pas du processus) et les fonctions de référence et d'association (rôle des mots et des configurations-étiquettes). Cette catégorisation permet de repérer l'importance relative des fonctions exercées par le langage dans les protocoles en tant qu'outil pour l'avancement du processus, et de repérer des conditions pour que ces fonctions se mettent en place et s'exercent.

Les motivations initiales de ce travail proviennent de l'étalonnage de caméras en vision artificielle. Nous nous sommes surtout intéressés aux manières d'exploiter des mesures dans les images (détection d'objets) et des considérations géométriques formelles. Nous avons élargi nos recherches à la problématique suivante :"l'interaction entre symbolique et numérique ". Ce travail se divise en trois parties. La première partie traite de la résolution d'équations polynomiales avec des coefficients approchés. Nous étudions des méthodes matricielles qui transforment la résolution en la recherche des valeurs et des vecteurs propres d'une matrice. Ces transformations et et les calculs de valeurs et vecteurs propres sont continues par rapport aux coefficients et permettent donc de résoudre des équations à coefficients approchés. La deuxième partie présente un cadre algébrique permettant d'exprimer simplement des contraintes géométriques. Ce formalisme nous a permis de modéliser de manière fine l'étalonnage d'une ou plusieurs caméras avec l'aide d'un plan. L'étalonnage ne peut être effectué pratiquement qu'avec des résolutions numériques de systèmes linéaires. La troisième partie est consacrée à l'étude et surtout à l'utilisation des outils de démonstration automatique en géométrie pour la construction de modèles 3D articulés. Par des optimisations numériques, nous déterminons les paramètres des modèles articulés qui permettent aux images de ces modèles de coïncider avec les données extraites des photographies

L'objet de cette thèse est d'étudier les capacités du système Coq à mélanger démonstrations et programmes en pratique en essayant d'y implémenter une part du programme Kenzo, un outil de calcul formel en algèbre homologique. À cet effet, nous travaillons sous trois contrainte: nous voulons essayer de lire le programme comme une démonstration avec un contenu calculatoire, ces démonstrations doivent calculer efficacement et nous cherchons à éviter de dupliquer des morceaux de démonstration. Nous montrons dans un premier temps comment le soucis d'efficacité conduit à reconsidérer certains aspects des mathématiques traditionnelle. Nous proposons une abstraction catégorielle adaptée, qui répond à la fois à un soucis de clareté et au besoin de partager les démonstration quand c'est possible. Cette abstraction, bien que différente des propositions traditionnelles, permet de formuler les notions d'algèbre homologique dans un style proche de celui de Kenzo. Nous proposons par ailleurs des modifications au programme de Coq pour rendre les démonstrations plus confortables, et pour permettre d'écrire des programmes plus efficaces. La première modification permet d'utiliser des tactiques plus fines, souvent nécessaire quand l'utilisation des types dépendents se fait commune. La seconde permet d'utiliser les capacité du processeur pour faire des calculs plus efficaces sur des entiers. Pour finir nous proposons quelques pistes pour améliorer le partage et la clareté du code. Malheureusement, nous nous heurtons aux limites du système. Nous montrons ainsi que Coq ne tiens pas forcément ses promesses et qu'il y aura besoin de travaux théoriques pour comprendre comment lever ces limites.

La logique linéaire fait désormais partie des outils standards en théorie de la démonstration et, de manière plus générale, dans l'étude de la correspondance de Curry-Howard. Nous présentons ici trois directions importantes d'application de méthodes issues de la logique linéaire : - la théorie de la démonstration de la logique classique et ses aspects calculatoires via notamment la sémantique des jeux ; - la complexité implicite à travers les modèles dénotationnels des logiques linéaires à complexité bornée ; - la théorie de la concurrence et ses fondements logiques grâce aux ingrédients apportés par la logique linéaire différentielle. Les approches linéaires offrent ainsi un cadre commun pour l'étude de différents aspects logiques du calcul.

Les défis pour voir des robots opérant dans l'environnement de tous les jours des humains et sur unelongue durée soulignent l'importance de leur adaptation aux changements qui peuvent être imprévisiblesau moment de leur construction. Ils doivent être capable de savoir quelles parties échantillonner, et quelstypes de compétences il a intérêt à acquérir. Une manière de collecter des données est de décider par soi-même où explorer. Une autre manière est de se référer à un mentor. Nous appelons ces deux manièresde collecter des données des modes d'échantillonnage. Le premier mode d'échantillonnage correspondà des algorithmes développés dans la littérature pour automatiquement pousser l'agent vers des partiesintéressantes de l'environnement ou vers des types de compétences utiles. De tels algorithmes sont appelésdes algorithmes de curiosité artificielle ou motivation intrinsèque. Le deuxième mode correspond au guidagesocial ou l'imitation, où un partenaire humain indique où explorer et où ne pas explorer.Nous avons construit une architecture algorithmique intrinsèquement motivée pour apprendre commentproduire par ses actions des effets et conséquences variées. Il apprend de manière active et en ligne encollectant des données qu'il choisit en utilisant plusieurs modes d'échantillonnage. Au niveau du metaapprentissage, il apprend de manière active quelle stratégie d'échantillonnage est plus efficace pour améliorersa compétence et généraliser à partir de son expérience à un grand éventail d'effets. Par apprentissage parinteraction, il acquiert de multiples compétences de manière structurée, en découvrant par lui-même lesséquences développementale.

L’intérêt que porte ce mémoire à la méthodologie de la recherche aristotélicienne de la vérité le confine à un examen précis des étapes préliminaires de cette recherche, dans l’objectif de surmonter une conception trop simplifiée de l’opposition entre la science et l’opinion chez Aristote. S’ancrant dans une présentation des fonctions de la dialectique, telles que décrites par le philosophe dans les Topiques, cette enquête entend fournir une comparaison étroite entre les méthodes dialectique et apodictique. Plus précisément, elle est le lieu d’une déconstruction des préjugés qui sous-tendent une lecture traditionnelle des Seconds analytiques, selon laquelle (1) la méthode apodictique doit guider la recherche scientifique et (2) l’épistémologie d’Aristote est radicalement fondationnaliste. La lecture, alternative, de ce traité que propose ce mémoire lui permet d’assouplir les conditions imposées par Aristote aux prémisses du syllogisme apodictique, de manière à exploiter les nuances qui s’inscrivent dans la distinction qu’il opère entre le mieux connu par nature et le mieux connu pour nous. Ce faisant, la frontière entre la dialectique, qui part des idées accréditées, et l’apodictique, qui part de prémisses vraies, se révèle moins franche et la notion d’epistēmē, moins « scientifique » au sens moderne du terme. Enfin, cette lecture alternative des Seconds analytiques est mise à contribution pour l’examen de l’hypothèse, inspirée d’un essai d’Owen (1961), selon laquelle le chapitre II, 19 de ce traité fournirait les pistes de réflexion permettant d’élucider, en même temps que le rôle de l’induction, celui de la dialectique dans le cheminement vers les premiers principes. / The attention this master’s thesis gives to the aristotelian method towards truth confines it to a precise examination of the preliminary steps of this method, in order to distance itself from an over-simplified opposition between science and opinion in Aristotle. Starting from a presentation of the functions of dialectic, as described by the philosopher in the Topics, this inquiry intends to provide a close comparison between the methods of dialectic and demonstration. More precisely, it aims to deconstruct the presuppositions underlining a traditional reading of the Posterior analytics, according to which (1) demonstrative method should provide a guide for scientific research and (2) Aristotle’s epistemology is radically foundationalist. The alternative reading this study suggests to adopt allows it to ease the conditions imposed by Aristotle on the premises of apodictic syllogism, as ways to exploit the distinction he makes between what is better known by nature and what is better known for us. In doing so, the frontier between dialectic, which starts from accredited ideas, and demonstration, which starts from true premises, appears to be less opaque and the concept of epistēmē, less “scientific” in the modern sense. Finally, this alternative reading of the Posterior analytics is put to contribution in examining the hypothesis, inspired by an essay from Owen (1961), regarding the possibility for the last chapter (II, 19) of this treatise to help us elucidate, both at the same time, the role of induction and that of dialectic in the path towards truth.

Cet ouvrage est consacré au kantisme non orthodoxe de Friedrich-Albert Lange (1828-1875) et Hermann von Helmholtz (1821-1894) développé dans la seconde moitié du XIXe qui propose une révision psychophysique de l’épistémologie kantienne. On affirme que ce procédé n’aboutit pas à une réduction psychologique de la connaissance qui aurait pour conséquence d’éliminer une objectivité judicative (contrairement à ce que prétendent plusieurs commentateurs) ; en revanche, ce procédé apporte des modifications significatives aux conditions de possibilité nécessaires et universelles de l’expérience qui légitiment chez Kant une objectivité judicative. On démontre que l’épistémologie développée par ces deux auteurs peut être qualifiée de « naturalisme méthodologique » et partage avec l’épistémologie naturalisée développée au XXe siècle par Willard von Orman Quine (1908-2000) une série de stratégies argumentaires analogues qui expliquent essentiellement « how evidence relates to theory, and in what ways one's theory of nature transcends any available evidence. » (Quine, 1969, 83) Ainsi afin de soutenir qu’il existe une telle épistémologie naturalisée au XIXe siècle, on divise l’ouvrage en trois parties. La première section (chapitres premier et deuxième) introduit le concept de « naturalisme épistémologique » et étudie ses conséquences doctrinales et conceptuelles. La seconde section (chapitres troisième, quatrième et cinquième) argumente que l’inscription de l’épistémologie kantienne dans un cadre conceptuel naturalisé n’implique pas l’élimination d’une réflexion de second ordre sur les raisons qui légitiment une objectivité judicative au profit d’une simple étude des causes psychophysiques de la perception et des jugements qui s’y rapporte. La troisième section (chapitres sixième et septième) est consacrée à la question de l’objectivité des jugements logico-mathématiques et plus particulièrement à leur signification intuitive dans le cadre de l’expérience psychophysique. À partir de ces trois sections, on prétend pouvoir démontrer que l’épistémologie naturalisée de Helmholtz, Lange et Quine mobilise des stratégies argumentaires structurellement analogues malgré des contextes historiques et conceptuels radicalement différents. On retrouve à la fin de chaque section des remarques conclusives comparatives qui mettent en valeur (autant que faire se peut) ces stratégies argumentaires analogues utilisées au XIXe et au XXe siècle.

Ce mémoire consiste en une étude critique de la démonstration de l’existence d’un premier principe telle qu’elle est développée par Jean Duns Scot (v.1265-1308) dans les trois premiers chapitres de son Traité du premier principe. Le présent travail a pour objectif de déterminer, au moyen de principes et de critères rigoureux, si la preuve avancée par le Docteur Subtil constitue une véritable démonstration. Pour ce faire, ce mémoire se déploie en trois grandes parties. La première partie met au jour la méthode employée par Duns Scot dans le traité à l’étude et s’attèle à tracer les contours des cadres épistémologique et métaphysique scotistes sur lesquels s’appuie l’ensemble de son argumentation. Puis, la deuxième partie est consacrée à l’exposition générale de la démonstration scotiste de l’existence d’un premier principe dans les ordres d’efficience, de finalité et d’éminence. Enfin, la dernière partie correspond à un examen minutieux de l’ensemble de la preuve scotiste. Chaque argument est alors passé en revue et évalué à l’aune de principes et de critères clairement établis dans l’introduction de ce mémoire. Au terme de cet examen, il nous sera alors possible de montrer qu’à défaut de prouver l’existence en acte d’une nature unique qui soit à la fois cause efficiente première de tout être, fin ultime de toute chose et réalité souverainement parfaite, Duns Scot parvient tout de même à établir l’existence d’un premier principe de l’être. / This thesis consists in a critical study of Duns Scotus’ demonstration of the existence of a First Principle as developed in the first three chapters of his book A treatise on God as First Principle. The objective of this work is to determine, by means of rigorous principles and criteria, whether the proof advanced by the Subtle Doctor constitutes a true demonstration. The thesis is divided into three main parts. The first part highlights the method employed by Duns Scotus in the treatise under study and endeavors to trace the outlines of Scotus’ epistemological and metaphysical frameworks on which the whole of the argument is based. The second part is devoted to the general exposition of Duns Scotus’ demonstration of the existence of a first principle in the orders of efficiency, finality and eminence. Finally, the last part corresponds to a careful examination of the entire proof of Duns Scotus. Each argument is then reviewed and assessed against the principles and criteria clearly established in the introduction. At the end of this examination, it will then be possible for us to show that the demonstration of Duns Scotus failed to prove the actual existence of a unique nature which is both the first effective cause of all beings, the ultimate end of all things, and a supremely perfect reality, but nevertheless manages to demonstrate the existence of a first principle of being.