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

Malgré la notoriété de Gabriel Fauré, le style particulier de sa musique chambre reste encore difficile à appréhender par l’analyse. La construction formelle y est un réel sujet de questionnement. Tandis que certains analystes essaient d’attester son originalité en examinant en quoi elle s’éloigne de la tradition, d’autres proposent des analyses de la dynamique caractéristique de ses thèmes, dont le développement continu aboutit à la réalisation de la grande forme. Ces dernières se sont jusqu’à présent appuyées sur un corpus limité. Cette thèse se propose d’élargir le corpus aux cinq grandes œuvres de chambre pour cordes et piano – deux Quatuors op. 15 et 45, deux Quintettes op. 89 et 115 et le Trio op. 120 et d’y cerner la « dynamique formelle ». Après l’étude des témoignages de l’époque du compositeur qui permet de mettre en relief la conception de l’originalité formelle dans son œuvre, l’analyse porte sur l’agencement interne des thèmes et sur la réalisation de la grande forme à partir de l’étude des partitions mais aussi à l’aide d’une représentation donnée par un logiciel informatique qui permet de visualiser l’enveloppe dynamique et de repérer des climax. En révélant en quoi consiste ce processus, la présente thèse contribue à mieux rendre compte du style personnel de Fauré et de la façon dont il élabore une musique qui donne l’impression d’une progression et d’un développement continus se prolongeant jusqu’à la fin de l’œuvre. / Despite the notoriety of Gabriel Fauré’s musical style, the particular style of his chamber music still remains difficult to comprehend by analysis. Formal construction is a real subject of question. While some analysts try to attest to his originality by examining how it departs from tradition, others offer analyses of the dynamic characteristic of its themes, whose continuous development leads to the realization of large form. The latter have so far relied on a limited corpus of works. This thesis proposes to expand the corpus to the five large chamber works for strings and piano - two Quartets op. 15 and 45, two Quintets op. 89 and 115 and the Trio op. 120 in order to define the “formal dynamics.” After the study of testimonies from the composer's time that highlights the formal originality in his work, the subsequent analysis deals with the internal arrangement of themes and the realization of large form from the study of scores. I conduct my analysis with the help of graphic representation created by a computer software that can visualize the enveloping dynamic and identify climaxes. By revealing the contents of this process, this thesis helps to better reflect the very personal style of Fauré and the way in which he creates music that gives the impression of continuous progression and development extending to the end of the work.

En planification théorique de la décision, le cadre des Processus Décisionnels Markoviens Factorisés (Factored Markov Decision Process, FMDP) a produit des algorithmes efficaces de résolution des problèmes de décisions séquentielles dans l'incertain. L'efficacité de ces algorithmes repose sur des structures de données telles que les Arbres de Décision ou les Diagrammes de Décision Algébriques (ADDs). Ces techniques de planification sont utilisées en Apprentissage par Renforcement par l'architecture SDYNA afin de résoudre des problèmes inconnus de grandes tailles. Toutefois, l'état-de-l'art des algorithmes d'apprentissage, de programmation dynamique et d'apprentissage par renforcement utilisés par SDYNA, requière que le problème soit spécifié uniquement à l'aide de variables binaires et/ou utilise des structures améliorables en termes de compacité. Dans ce manuscrit, nous présentons nos travaux de recherche visant à élaborer et à utiliser une structure de donnée plus efficace et moins contraignante, et à l'intégrer dans une nouvelle instance de l'architecture SDYNA. Dans une première partie, nous présentons l'état-de-l'art de la modélisation de problèmes de décisions séquentielles dans l'incertain à l'aide de FMDP. Nous abordons en détail la modélisation à l'aide d'DT et d'ADDs.Puis nous présentons les ORFGs, nouvelle structure de données que nous proposons dans cette thèse pour résoudre les problèmes inhérents aux ADDs. Nous démontrons ainsi que les ORFGs s'avèrent plus efficaces que les ADDs pour modéliser les problèmes de grandes tailles. Dans une seconde partie, nous nous intéressons à la résolution des problèmes de décision dans l'incertain par Programmation Dynamique. Après avoir introduit les principaux algorithmes de résolution, nous nous attardons sur leurs variantes dans le domaine factorisé. Nous précisons les points de ces variantes factorisées qui sont améliorables. Nous décrivons alors une nouvelle version de ces algorithmes qui améliore ces aspects et utilise les ORFGs précédemment introduits. Dans une dernière partie, nous abordons l'utilisation des FMDPs en Apprentissage par Renforcement. Puis nous présentons un nouvel algorithme d'apprentissage dédié à la nouvelle structure que nous proposons. Grâce à ce nouvel algorithme, une nouvelle instance de l'architecture SDYNA est proposée, se basant sur les ORFGs ~:~l'instance SPIMDDI. Nous testons son efficacité sur quelques problèmes standards de la littérature. Enfin nous présentons quelques travaux de recherche autour de cette nouvelle instance. Nous évoquons d'abord un nouvel algorithme de gestion du compromis exploration-exploitation destiné à simplifier l'algorithme F-RMax. Puis nous détaillons une application de l'instance SPIMDDI à la gestion d'unités dans un jeu vidéo de stratégie en temps réel. / In decision theoretic planning, the factored framework (Factored Markovian Decision Process, FMDP) has produced several efficient algorithms in order to resolve large sequential decision making under uncertainty problems. The efficiency of this algorithms relies on data structures such as decision trees or algebraïc decision diagrams (ADDs). These planification technics are exploited in Reinforcement Learning by the architecture SDyna in order to resolve large and unknown problems. However, state-of-the-art learning and planning algorithms used in SDyna require the problem to be specified uniquely using binary variables and/or to use improvable data structure in term of compactness. In this book, we present our research works that seek to elaborate and to use a new data structure more efficient and less restrictive, and to integrate it in a new instance of the SDyna architecture. In a first part, we present the state-of-the-art modeling tools used in the algorithms that tackle large sequential decision making under uncertainty problems. We detail the modeling using decision trees and ADDs. Then we introduce the Ordered and Reduced Graphical Representation of Function, a new data structure that we propose in this thesis to deal with the various problems concerning the ADDs. We demonstrate that ORGRFs improve on ADDs to model large problems. In a second part, we go over the resolution of large sequential decision under uncertainty problems using Dynamic Programming. After the introduction of the main algorithms, we see in details the factored alternative. We indicate the improvable points of these factored versions. We describe our new algorithm that improve on these points and exploit the ORGRFs previously introduced. In a last part, we speak about the use of FMDPs in Reinforcement Learning. Then we introduce a new algorithm to learn the new datastrcture we propose. Thanks to this new algorithm, a new instance of the SDyna architecture is proposed, based on the ORGRFs : the SPIMDDI instance. We test its efficiency on several standard problems from the litterature. Finally, we present some works around this new instance. We detail a new algorithm for efficient exploration-exploitation compromise management, aiming to simplify F-RMax. Then we speak about an application of SPIMDDI to the managements of units in a strategic real time video game.

Lors de l’exploration d’espace de conception, les données résultantes de la simulation d’un grand nombre d’alternatives de conception peuvent conduire à la surcharge d’information quand il s’agit de choisir une bonne solution de conception. Cette exploration d’espace de conception s’apparente à une méthode d’optimisation en conception multicritère mais en mode manuel pour lequel des outils appropriés à la visualisation de données multidimensionnelle sont employés. Pour le concepteur, un processus en trois phases – découverte, optimisation, sélection – est suivi selon un paradigme dit de Design by Shopping. Le fait de « parcourir » l’espace de conception permet de gagner en intuition sur les sous-espaces de solutions faisables et infaisables et sur les solutions offrant de bons compromis. Le concepteur apprend au cours de ces manipulations graphiques de données. La sélection d’une solution optimale se fait donc sur la base d’une décision dite informée. L’objectif de cette recherche est la performance des représentations graphiques pour l’exploration d’espace de conception, pour les trois phases du processus en Design by Shopping. Pour cela, cinq représentations graphiques, identifiées comme potentiellement performantes, sont testées à travers deux expérimentations. Dans la première, trente participants ont testé trois graphiques, pour la phase de sélection dans une situation multi-attribut, à travers trois scénarios de conception où une voiture doit être choisie parmi quarante selon des préférences énoncées. Pour cela, un indice de qualité est proposé pour calculer la qualité de la solution du concepteur pour un des trois scénarios définis, la solution optimale selon cet indice étant comparée à celles obtenues après manipulation des graphiques. Dans la deuxième expérimentation, quarante-deux concepteurs novices ont résolu deux problèmes de conception à l’aide de trois graphiques. Dans ce cas, la performance des graphiques est testée pour la prise de décision informée et pour les trois phases du processus dans une situation multi-objectif. Les résultats révèlent qu’un graphique est adapté à chacune des trois phases du Design by Shopping :: le graphique Scatter Plot Matrix pour la phase de découverte et pour la prise de décision informée, le graphique Simple Scatter pour la phase d’optimisation et le graphique Parallel Coordinate Plot pour la phase de sélection aussi bien dans une situation multi-attribut que multi-objectif. / In Design space exploration, the resulting data, from simulation of large amount of new design alternatives, can lead to information overload when one good design solution must be chosen. The design space exploration relates to a multi-criteria optimization method in design but in manual mode, for which appropriate tools to support multi-dimensional data visualization are employed. For the designer, a three-phase process - discovery, optimization, selection - is followed according to a paradigm called Design by Shopping. Exploring the design space helps to gain insight into both feasible and infeasible solutions subspaces, and into solutions presenting good trade-offs. Designers learn during these graphical data manipulations and the selection of an optimal solution is based on a so-called informed decision. The objective of this research is the performance of graphs for design space exploration according to the three phases of the Design by Shopping process. In consequence, five graphs, identified as potentially efficient, are tested through two experiments. In the first, thirty participants tested three graphs, in three design scenarios where one car must be chosen out of a total of forty, for the selection phase in a multi-attribute situation where preferences are enounced. A response quality index is proposed to compute the choice quality for each of the three given scenarios, the optimal solutions being compared to the ones resulting from the graphical manipulations. In the second experiment, forty-two novice designers solved two design problems with three graphs. In this case, the performance of graphs is tested for informed decision-making and for the three phases of the process in a multi-objective situation. The results reveal three efficient graphs for the design space exploration: the Scatter Plot Matrix for the discovery phase and for informed decision-making, the Simple Scatter Plot for the optimization phase and the Parallel Coordinate Plot for the selection phase in a multi-attribute as well as multi-objective situation.