Une technique d'abstraction et de partage de structure pour une methode de démonstration automatique non expérimentée jusqu'à présent est proposée. On donne aussi une généralisation de la règle d'inférence pour le cas propositionnel. Une preuve est séparée en plan + validation, ce qui correspond à séparer la partie purement déductive de l'algorithme d'unification. Cette séparation est utilisée pour détecter les ensembles responsables des échecs de validation pour un retour arrière non aveugle

Cette thèse présente un calcul des séquents pour la logique linéaire enrichie d'un connecteur non commutatif et autodual "précède" situé entre le "par" et le "tenseur". Il est défini pour des séquents dont les formules sont orientées par un ordre partiel. Un calcul de réseaux de démonstration quotientant ce calcul des séquents est défini en termes de graphes orientés. Ce calcul est doté d'une sémantique dénotationnelle dans les espaces cohérents, préservée par élimination des coupures, un processus convergent et confluent. Des résultats combinatoires nécessaires sur les ordres partiels et sur la structure des graphes de démonstrations sont établies ainsi que quelques propriétés du calcul commutatif avec la règle MIX.

Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

Présentation d'une approche déductive basée sur l'instantiation progressive de schémas de programmes fonctionnels. Un système formel de preuve est décrit dans lequel le lien entre schémas de programmes et schémas de propriétés est exhibe. La complétude relative et la correction de ce système sont prouvées notamment pour les fonctions partiellement définies. Des stratégies, guidées par l'utilisateur, sont ensuite proposées qui permettent de caractériser les propriétés nécessaires, propres à chaque schema, en termes de recherche de préconditions

Après un historique bref et général de la déduction automatique, on analyse les tendances actuelles et les besoins en présentation de preuves et communication d'outils d'inférence. Les notions théoriques concernées sont présentées et étudiées en détail. On donne ensuite une synthèse comparative critique et exhaustive de l'état de l'art. Cette synthèse manquait dans la littérature. L'analyse des notions fondamentales en logique et la synthèse sur l'état de l'art permettent d'établir les caractéristiques retenues pour le système GLEF (Graphical & Logical Edition Framework). La conception et la réalisation de deux langages ont permis de rendre GLEF générique (c'est à dire paramétrable par le système formel employé et par la présentation de ses preuves). Un formalisme de définition, fondé sur le Calcul des Construction (dû à Coquand et Huet), sert à représenter et à vérifier les systèmes formels et les preuves dans ses systèmes formels. Un langage de présentation, fondé sur la notion de «boîte», sert à décrire leur présentation. En annexe nous donnons un algorithme original pour l'opération d'effacement, particulièrement difficile en lambda-calcul typé, qui sert à réaliser la commande «couper» de GLEF. GLEF a été développé au sein du projet ATINF (ATelier d'INFérence). Un manuel utilisateur rudimentaire et de nombreux exemples d'utilisation en sont donnés. Certains exemples montrent comment, après avoir spécifié la définition et la présentation d'un système formel objet, un utilisateur de GLEF peut construire ou visualiser des preuves en manipulant directement les objets (formules, preuves partielles, etc.) à l'écran, avec la souris. D'autres illustrent comment GLEF présente les preuves produites par les démonstrateurs d'ATINF ou extérieurs à ATINF. Les principales lignes de recherche future concluent ce travail

Etude des résolutions de problèmes mathématiques par des personnes parvenues au stade hypothético-déductif exprimées par un discours. Présentation d'un outil pour l'étude des raisonnements naturels.

.

La question principale de cette thèse est la pertinence de l’utilisation d’humains virtuel pour l’enseignement de geste moteur. Une première étude explore la question de la faisabilité d’un apprentissage par l’imitation d’un humain virtuel. Pour ce faire, l’amélioration de performance de trois gestes de karaté par trois groupes s’entraînant dans différents environnements est évaluée. Une classe traditionnel de karaté, un enseignement par vidéo et un enseignement en réalitévirtuel sont comparé. Une seconde étude évalue l’influence d’une représentation de soi dans l’environnement virtuel sur la réalisation de la tâche d’apprentissage. Les participants à cette étude ont un retour visuel de leur action sous la forme d’un avatar cylindrique représenté dans un miroir de l’environnement virtuel. L’influence de cet avatar sur la tâche d’apprentissage est évalué de deux façon : 1) par l’évaluation externe de la performance 2) par le biais d’entretiens d’explicitation qui permettentd’obtenir le point de vue du participant. Ces deux études sont complétées par une troisième étude qui évalue un outil d’évaluation automatique de la performance. Cet outil est conçue dans le but d’éliminer les biais créés par un évaluateur humain. Un tel outil est nécessaire afin de pouvoir comparer les quatre environnements d’apprentissage présentés dans cette thèse ainsi que ceux qui seront créé dans le futur. En effet, seul un évaluateur automatique peut être parfaitement consistent sur toute la durée des études.En conclusion, ces études ont permit d’établir que l’apprentissage par l’imitation d’un humain virtuel est possible. En conséquence, l’utilisation d’humains virtuels pour l’enseignement de gestes moteurs est pertinente. Ces environnements peuvent être utiles à plusieurs fins. Ils peuvent servir d’environnements contrôles pour l’étude de l’apprentissage par imitation. Le protocole développé dans cette étude peut être utilisé dans une boucle itérative pour le développementde version subséquentes d’environnements virtuel ou d’accélérateurs d’entraînement virtuel. Ce protocole peut également être utilisé pour le développement de jeux vidéos actifs plus efficaces pour combattre la sédentarité et la crise mondiale d’obésité qui y est rattachée / The main question of that thesis is on the relevance of using virtual humans to teach complex motor skills. The first study explores the question of the feasibility of learning by imitation of a virtual human by comparing the improvement of the performance on three karate gestures for three groups, namely a traditional class, a video-based group and a virtual reality group. The second study investigates the influence on the learning task of having a self representation in the virtual environment. The participants have a feedback of their movements represented on a mirrored cylindrical gray avatar. The impact of that avatar on the learning task of the participants is assessed by two means. Performance evaluations are performed and give an external perspective on the learning. Evocation interview are also performed to get an insight of the learning task from the participants point of view. Finally, these two studies are completed by a third one investigating the possibility to have an automatic performance evaluator in order to reduce grading discrepancies generated by humans graders. Such a tool would be required to have an objective performance evaluation of all the participants in order to compare the four learning environments presented in that thesis and eventual further iteration of these environments. The conclusion our the studies presented in that thesis are that learning motor skills from the imitation of a virtual human is possible. Consequently, virtual learning environments for motorskills teaching are relevant. Furthermore, these environments can be used in various types of applications. They can be used as a study tool for standard and controlled investigation of teaching by demonstration. They can also be used in an engineering loop for the development of further learning environments and training accelerators. They also have a potential usage in the development of exergames in response to the international obesity crisis

Cette thèse porte sur l'étude théorique et pratique d'un système de typage appliqué à la preuve de programmes de style fonctionnels. Le système de base est le système ST créé par C.Raffalli; il comporte, outre le polymorphisme, du sous-typage et de l'omission de contenu non-algorithmique. Nous étudions tout d'abord les modèles de la théorie définie par le système de types, en construisant une axiomatique basée sur les treillis permettant de modéliser le calcul et la logique. Nous étudions sur cette base le système de types, montrons la réduction du sujet, et la possibilité de définir en interne la normalisabilité et la réductibilité des programmes. Dans la suite de la thèse, plus appliquée, nous étudions des codages de types de données riches inspirés des langages fonctionnels - y incluant notamment un système de modules du premier ordre- dans le Lambda-Calcul, et montrons qu'ils s'intègrent harmonieusement dans le système; la méthodologie développée dans cette partie permet d'étendre le langage de types et le langage de programmation en conservant un critère de consistance assurant la sûreté du code typé.

Cette Thèse est la conclusion de trois ans de travail sur un projet nommé DemoNat. Le but de ce projet est la conception d'un système d'analyse et de vérification de démonstrations mathématiques écrites en langue naturelle.<br><br>L'architecture générale du système se décrit en 4 phases :<br>- analyse de la démonstration par des outils linguistiques ;<br>- traduction de la démonstration dans un langage restreint ;<br>- interprétation du texte traduit en un arbre de règles de déduction ;<br>- validation des règles de déduction à l'aide d'un démonstrateur automatique.<br><br>Ce projet a mobilisé des équipes de linguistes et de logiciens, les deux premières phases étant la tâche des linguistes, et les deux dernières étant la tâche des logiciens.<br><br>Cette thèse présente plus en détail ce projet et développe principalement les points suivants :<br>- définition du langage restreint et de son interprétation ;<br>- propriétés du type principal de termes d'un lambda-calcul typé avec deux flèches entrant dans le cadre d'un outil linguistique, les ACGs ;<br>- description du démonstrateur automatique.