Cette thèse étudie comment l'intégration du calcul dans les démonstrations peut les simplifier. Nous nous intéressons pour cela à la déduction modulo et à la surdéduction, deux formalismes proches dans lesquels le calcul est incorporé dans les démonstrations via un système de réécriture. Pour améliorer la recherche mécanisée de démonstration, nous considérons trois critères de simplicité. L'admissibilité des coupures permet de restreindre l'espace de recherche des démonstrations, mais elle n'est pas toujours assurée en déduction modulo. Nous définissons une procédure qui complète le système de réécriture pour, au final, admettre les coupures. Au passage, nous montrons comment transformer toute théorie pour l'intégrer à la partie calculatoire des démonstrations. Nous montrons ensuite comment la déduction modulo permet de réduire arbitrairement la taille des démonstrations, en transférant des étapes de déduction dans le calcul. En particulier, nous appliquons ceci à l'arithmétique d'ordre supérieur pour démontrer que les réductions de taille qui sont possibles en augmentant l'ordre dans lequel on se place disparaissent si on travaille en déduction modulo. Suite à ce dernier résultat, nous avons recherchés quels sont les systèmes d'ordre supérieur pouvant être simulés au premier ordre, en déduction modulo. Nous nous sommes intéressés aux systèmes de type purs et nous montrons comment ils peuvent être encodés en surdéduction, ce qui offre de nouvelles perspectives concernant leur normalisation et la recherche de démonstration dans ceux-ci. Nous développons également une méthodologie qui permet d'utiliser la surdéduction pour spécifier des systèmes de déduction. / This thesis study how computations may simplify proofs and aims to make mechanized proof search better. We are particularly interested in deduction modulo and superdeduction, two close formalisms allowing the integration of computations into proofs through a rewrite system. We consider three simplicity criteria related to proof search. Cut admissibility makes it possible to restrain the proof-search space but does not always hold in deduction modulo. We define a completion method transforming a rewrite system representing computations so that at the end cut admissibility holds. By the way, we show how to transform any first-order theory to integrate it into the computational part of proofs. We show then how deduction modulo unboundedly reduces proof lengths, by transferring deduction steps into computations. In particular, we apply this to higher-order arithmetic to show that proof-length speedups between ith- and i+1st-order arithmetic disappear when working in deduction modulo, making it possible to work in first-order logic modulo without increasing proof lengths. Following this last result, we investigate which higher-order systems can be simulated in first order using deduction modulo. We are interested by pure type systems, which are generic type systems for the lambda-calculus with dependent types. We show how these systems can be encoded in superdeduction. This offers new perspectives on their normalization and on proof search within them. We also develop a methodology to describe how superdeduction can be used to specify deductive systems.

Cette thèse présente une nouvelle édition critique de quatre discours de Libanios : les discours 34 (En réponse aux médisances du pédagogue), 35 (À ceux qui ne prennent pas la parole), 36 (Sur les maléfices), et 43 (Sur la convention), ainsi que de nouvelles traductions commentées. Ce premier ensemble est complété par des études thématiques prenant en compte la dimension rhétorique et historique de ces textes. Le corpus libanien a joué un rôle déterminant dans l’émergence et le développement des études sur l’Antiquité tardive. Une nouvelle approche de ces quatre textes offre un intérêt indiscutable pour la connaissance du monde scolaire de cette époque : ils délivrent un grand nombre d’informations sur l’univers et le statut des maîtres de rhétorique, sur le rôle social de l’école et la place de la rhétorique dans l’enseignement. Ils constituent ainsi une source très riche pour l’histoire institutionnelle, culturelle et sociale du IVe siècle ap. JC. Leur contribution à l’histoire de l’espace urbain d’Antioche, champ de recherche actuellement en cours d’exploration, ne doit pas non plus être dédaignée. / This thesis presents a new critical edition of four orations by Libanius : oration 34 (in response to the pedagogue’s badmouthing), 35 (To those who do not speak), 36 (About witchcraft) and 43 (About the convention) and new translations with commentaries. This first set is completed by thematic studies taking into account the rhetoric and historical dimension of these texts. The Libanius corpus played a key role in the emergence and development of Late Antiquity studies. A new approach to these four texts offers an undisputable interest for the knowledge of the school world of that time; they issue indeed a lot of information about the world and the status of teachers of rhetoric, on the social role of the school and the place of rhetoric in education. They constitute a very rich source for institutional, cultural and social history of the 4th century AD. Their contribution to the history of the urban area of Antioch, search field currently being explored, should not be left out.

En élaborant le présent mémoire, nous avons cherché à mieux comprendre comment se développe la notion de preuve dans le cheminement d'apprentissage d'un élève du secondaire. Dans cette optique, nous avons d'abord fait le point sur notre propre expérience d'enseignement et sur nos réflexions personnelles, suscitées entre autres par deux expérimentations conduites par nous dans le cadre du cours d'Initiation à la recherche en didactique des mathématiques. Nous avons ensuite cherché à retracer quels objectifs des programmes du MEQ se rapportent à l'apprentissage de la preuve, et que suggèrent ces programmes pour que ces objectifs soient atteints. Nous avons pu constater que cet apprentissage y passe avant tout par l'étude de la géométrie. La lecture de deux articles de R. Thom et R. Bkouche nous a permis de mieux cerner les liens privilégiés entre géométrie et apprentissage de la preuve. Ceux-ci sont profonds, incontournables, entre autres parce que les concepts et raisonnements géométriques occupent une position charnière entre le « sensible » et le « formel ». Nous avons alors arrêté l'objet précis de notre étude : l'apprentissage de la preuve, tel que véhiculé par les problèmes de géométrie synthétique, dans une collection du secondaire. Dans le but d'élaborer une grille d'analyse, nous avons dégagé la notion de « schéma de bipolarisation » des réflexions sur la preuve d'É. Barbin, de G. Hanna, G. Brousseau, N. Balacheff et N. Rouche. À partir des schémas de bipolarisation suggérés par leurs travaux, nous avons édifié notre propre typologie des preuves et par suite, notre grille d'analyse des problèmes. Après une classification des problèmes de la collection à l'étude selon cette grille, nous avons interprété et analysé cette classification, pour conclure sur les aspects de l'apprentissage de la preuve que nous évaluons comme mal « gérés » dans la collection : transition non suffisamment graduelle du sensible au formel (très peu de problèmes qui sollicitent une validation hybride, niveau de formalisation trop longtemps stationnaire, rôle ambigu de la géométrie des transformations dans le processus de formalisation, etc.), prépondérance des applications directes et des déductions locales sur les séquences déductives, intérêt et mode de présentation des résultats qui ne favorisent pas une « attitude de preuve », etc.

Cette thèse s'inscrit dans le cadre de l'apprentissage par renforcement pour les systèmes de dialogue. Ce document propose différentes manières de considérer l'être humain, interlocuteur du système de dialogue. Après un aperçu des limites du cadre agent/environnement traditionnel, nous proposons de modéliser dans un premier temps le dialogue comme un jeu stochastique. Dans ce cadre, l'être humain n'est plus vu comme une distribution de probabilité stationnaire mais comme un agent cherchant à optimiser ses préférences. Nous montrons que ce cadre permet une prise en compte de phénomènes de co-adaptation intrinsèques au dialogue humain/machine et nous montrons que ce cadre étend le champ d'application des systèmes de dialogue, par exemple aux dialogues de négociations. Dans un second temps, nous présentons une méthode permettant à l'être humain d'accélérer et de sécuriser la phase d'apprentissage de son système de dialogue par le biais de conseils encodés sous la forme d'une fonction de récompense. Nous montrons que cette prise en compte de conseils permet de significativement améliorer les performances d'un agent apprenant par renforcement. Finalement, une troisième situation est considérée. Ici, un système écoute une conversation entre humains et agit de manière à influer sur le cours de la conversation. Une fonction de récompense originale permettant de maximiser le résultat de la conversation tout en minimisant l'intrusivité du système est proposé. Nous montrons que notre approche permet de significativement améliorer les conversations. Pour implémenter cette approche, un modèle de la conversation est requis. C'est pourquoi nous proposons dans une quatrième contribution d'apprendre ce modèle à partir d'un algorithme d'apprentissage d'automates à multiplicité. / The context of this thesis takes place in Reinforcement Learning for Spoken Dialogue Systems. This document proposes several ways to consider the role of the human interlocutor. After an overview of the limits of the traditional Agent/Environment framework, we first suggest to model human/machine dialogue as a Stochastic Game. Within this framework, the human being is seen as a rational agent, acting in order to optimize his preferences. We show that this framework allows to take into consideration co-adaptation phenomena and extend the applications of human/machine dialogue, e.g. negociation dialogues. In a second time, we address the issue of allowing the incorporation of human expertise in order to speed-up the learning phase of a reinforcement learning based spoken dialogue system. We provide an algorithm that takes advantage of those human advice and shows a great improvement over the performance of traditional reinforcement learning algorithms. Finally, we consider a third situation in which a system listens to a conversation between two human beings and talk when it estimates that its intervention could help to maximize the preferences of its user. We introduce a original reward function balancing the outcome of the conversation with the intrusiveness of the system. Our results obtained by simulation suggest that such an approach is suitable for computer-aided human-human dialogue. However, in order to implement this method, a model of the human/human conversation is required. We propose in a final contribution to learn this model with an algorithm based on multiplicity automata.

La théorie des AMAS (Adaptive Multi-Agent Systems) propose de résoudre des problèmes complexes par auto-organisation pour lesquels aucune solution algorithmique n'est connue. Le comportement auto-organisateur des agents coopératifs permet au système de s'adapter à un environnement dynamique pour maintenir le système dans un état de fonctionnement adéquat. Dans cette thèse, cette approche a été appliquée au contrôle dans les systèmes ambiants, et plus particulièrement à la robotique de service. En effet, la robotique de service tend de plus en plus à s'intégrer à des environnements ambiants, on parle alors de robotique ambiante. Les systèmes ambiants présentent des caractéristiques, telles que l'ouverture et l'hétérogénéité, qui rendent la tâche de contrôle particulièrement complexe. Cette complexité est accrue si l'on prend en compte les besoins spécifiques, changeants et parfois contradictoires des utilisateurs. Les travaux de cette thèse proposent d'utiliser les principes de l'auto-organisation, pour concevoir un système multi-agent capable d'apprendre en temps réel à contrôler un système à partir des démonstrations faites par un tuteur. C'est l'apprentissage par démonstration. En observant l'activité de l'utilisateur et en apprenant le contexte dans lequel l'utilisateur agit, le système apprend une politique de contrôle pour satisfaire les utilisateurs. Nous proposons un nouveau paradigme de conception des systèmes robotiques sous le nom d'Extreme Sensitive Robotics. L'idée de base de ce paradigme est de distribuer le contrôle au sein des différentes fonctionnalités qui composent un système et de doter chacune de ces fonctionnalités de la capacité à s'adapter de manière autonome à son environnement. Pour évaluer l'apport de ce paradigme, nous avons conçu ALEX (Adaptive Learner by EXperiments), un système multi-agent adaptatif dont la fonction est d'apprendre, en milieux ambiants, à contrôler un dispositif robotique à partir de démonstrations. L'approche par AMAS permet la conception de logiciels à fonctionnalités émergentes. La solution à un problème émerge des interactions coopératives entre un ensemble d'agents autonomes, chaque agent ne possédant qu'une vue partielle de l'environnement. L'application de cette approche nous conduit à isoler les différents agents impliqués dans le problème du contrôle et à décrire leurs comportements locaux. Ensuite, nous identifions un ensemble de situations de non coopération susceptibles de nuire à leurs comportements et proposons un ensemble de mécanismes pour résoudre et anticiper ces situations. Les différentes expérimentations ont montré la capacité du système à apprendre en temps réel à partir de l'observation de l'activité de l'utilisateur et ont mis en évidence les apports, les limitations et les perspectives offertes par notre approche à la problématique du contrôle de systèmes ambiants. / The AMAS (Adaptive Multi-Agent Systems) theory proposes to solve complex problems for which there is no known algorithmic solution by self-organization. The self-organizing behaviour of the cooperative agents enables the system to self-adapt to a dynamical environment to maintain the system in a functionality adequate state. In this thesis, we apply the theory to the problematic of control in ambient systems, and more particularly to service robotics. Service robotics is more and more taking part in ambient environment, we talk of ambient robotics. Ambient systems have challenging characteristics, such as openness and heterogeneity, which make the task of control particularly complex. This complexity is increased if we take into account the specific, changing and often contradictory needs of users. This thesis proposes to use the principle of self-organization to design a multi-agent system with the ability to learn in real-time to control a robotic device from demonstrations made by a tutor. We then talk of learning from demonstrations. By observing the activity of the users, and learning the context in which they act, the system learns a control policy allowing to satisfy users. Firstly, we propose a new paradigm to design robotic systems under the name Extreme Sensitive Robotics. The main proposal of this paradigm is to distribute the control inside the different functionalities which compose a system, and to give to each functionality the capacity to self-adapt to its environment. To evaluate the benefits of this paradigm, we designed ALEX (Adaptive Learner by Experiments), an Adaptive Multi-Agent System which learns to control a robotic device from demonstrations. The AMAS approach enables the design of software with emergent functionalities. The solution to a problem emerges from the cooperative interactions between a set of autonomous agents, each agent having only a partial perception of its environment. The application of this approach implies to isolate the different agents involved in the problem of control and to describe their local behaviour. Then, we identify a set of non-cooperative situations susceptible to disturb their normal behaviour, and propose a set of cooperation mechanisms to handle them. The different experimentations have shown the capacity of our system to learn in realtime from the observation of the activity of the user and have enable to highlight the benefits, limitations and perspectives offered by our approach to the problematic of control in ambient systems.

Les robots modernes sont appelés à effectuer des opérations ou tâches complexes et la capacité de navigation autonome dans un environnement dynamique est un besoin essentiel pour les robots mobiles. Dans l’objectif de soulager de la fastidieuse tâche de préprogrammer un robot manuellement, cette thèse contribue à la conception de commande intelligente afin de réaliser l’apprentissage des robots mobiles durant la navigation autonome. D’abord, nous considérons l’apprentissage des robots via des démonstrations d’experts. Nous proposons d’utiliser un réseau de neurones pour apprendre hors-ligne une politique de commande à partir de données utiles extraites d’expertises. Ensuite, nous nous intéressons à l’apprentissage sans démonstrations d’experts. Nous utilisons l’apprentissage par renforcement afin que le robot puisse optimiser une stratégie de commande pendant le processus d’interaction avec l’environnement inconnu. Un réseau de neurones est également incorporé et une généralisation rapide permet à l’apprentissage de converger en un certain nombre d’épisodes inférieur à la littérature. Enfin, nous étudions l’apprentissage par fonction de récompenses potentielles compte rendu des démonstrations d’experts optimaux ou non-optimaux. Nous proposons un algorithme basé sur l’apprentissage inverse par renforcement. Une représentation non-linéaire de la politique est désignée et la méthode du max-margin est appliquée permettant d’affiner les récompenses et de générer la politique de commande. Les trois méthodes proposées sont évaluées sur des robots mobiles afin de leurs permettre d’acquérir les compétences de navigation autonome dans des environnements dynamiques et inconnus / Modern robots are designed for assisting or replacing human beings to perform complicated planning and control operations, and the capability of autonomous navigation in a dynamic environment is an essential requirement for mobile robots. In order to alleviate the tedious task of manually programming a robot, this dissertation contributes to the design of intelligent robot control to endow mobile robots with a learning ability in autonomous navigation tasks. First, we consider the robot learning from expert demonstrations. A neural network framework is proposed as the inference mechanism to learn a policy offline from the dataset extracted from experts. Then we are interested in the robot self-learning ability without expert demonstrations. We apply reinforcement learning techniques to acquire and optimize a control strategy during the interaction process between the learning robot and the unknown environment. A neural network is also incorporated to allow a fast generalization, and it helps the learning to converge in a number of episodes that is greatly smaller than the traditional methods. Finally, we study the robot learning of the potential rewards underneath the states from optimal or suboptimal expert demonstrations. We propose an algorithm based on inverse reinforcement learning. A nonlinear policy representation is designed and the max-margin method is applied to refine the rewards and generate an optimal control policy. The three proposed methods have been successfully implemented on the autonomous navigation tasks for mobile robots in unknown and dynamic environments.

No description available.