L’apprentissage associatif est un mécanisme d’une grande complexité, faisant appel à plusieurs processus à la fois. Le processus attentionnel est un des premiers à être mobilisé lors d’une association, il serait même impliqué pour extraire les paramètres temporels associés à un stimulus inconditionnel biologiquement signifiant avant même toute association effective (Balsam, Drew, and Yang, 2002). Certains travaux ont montré l’implication de certaines structures neurobiologiques à travers lesquelles les effets du processus attentionnel pourraient se mettre en place. Pour l’équipe de Holland PC, par exemple, les réponses d’orientation vers un stimulus conditionné (attention top-down)(Lee et al., 2005), impliquent le noyau central de l’amygdale ainsi que les projections dopaminergiques nigro-striées tandis qu’une présentation d’un nouveau stimulus de façon imprévue lors d’une association (attention bottom-up) mobilisera plutôt la substancia inominata qui serait modulé par le noyau central de l’amygdale (CeA) et le cortex pariétal (Holland and Gallagher, 2006). Parallèlement, le processus attentionnel dans une discrimination temporelle, dans lequel l’apprentissage associatif nécessite, outre des stimuli sensoriels discrets, des performances liées au jugement des durées. Dans ce dernier cas, le mécanisme du processus attentionnel mobilise d’autres modèles conceptuels qui gravitent principalement autour du modèle d’horloge interne et en particulier le modèle du striatal beat frequency pour l’explication neurobiologique (Matell and Meck, 2004).Dans le présent travail, nous avions pour ambition de comprendre le rôle de la voie Amygdalo-nigro-striée (ANS) dans la mise en place du processus attentionnel dans un apprentissage associatif orienté vers un stimulus sensoriel discret comme temporel chez le rat. Nous voulions également examiner le rôle de cette voie dans l’évolution du processus attentionnel après surentraînement ou automatisation. Pour la réalisation de cet objectif, nous avons comparé les effets des lésions croisées du CeA dans un hémisphère et la voie nigro-striée dans l’autre hémisphère (disconnection de la voie amygdalo-nigro-striée ; groupe Contra), avec des lésions du CeA et de la voie nigro-striée dans le même hémisphère (groupe Ipsi). Un troisième groupe a fait l’objet d’une lésion bilatérale du CeA seulement (groupe Amy) et un quatrième groupe n’est pas lésé. A travers nos trois groupes expérimentaux (Contra, Ipsi et Amy) et notre groupe contrôle (Sham), nous avons montré l’implication du CeA dans la modulation du processus attentionnel au moment d’un changement dans la situation expérimentale (surprise), aussi bien en présence d’un stimulus sensoriel discret appétitif que d’un stimulus temporel dans un contexte aversif. Nous avons également montré que la voie ANS est impliquée dans la mise en place de l’automatisation et que probablement il y a un effet différenciel entre la partie postérieure et antérieure du CeA. Nos travaux ont mis également en évidence l’implication de la voie nigro-striée dans la discrimination temporelle et de la voie ANS dans le traitement attentionnel dans des tâches de perception temporelle. Ce traitement est différent selon si le jugement concerne des durées courtes ou durées longues. / Associative learning is a highly complex mechanism, involving several processes at the same time. The attentional process is one of the first to be mobilized during an association; it would also be involved to extract the temporal parameters associated with an unconditional biologically meaningful stimulus even before any effective association (Balsam, Drew, and Yang 2002). Some studies have shown the involvement of certain neurobiological structures, which may underlie attentional processes. For the Holland PC team, for example, orientation responses to a conditioned stimulus (top-down attention) (Lee et al., 2005) involve the central nucleus and nigro-striatal dopaminergic projections, whereas presentation of a new stimulus during an association (bottom-up attention) would rather imply the substancia inominata which would be modulated by the central nucleus of amygdala (CeA) and the parietal cortex (Holland and Gallagher 2006). At the same time, in temporal discrimination in which associative learning requires, besides discrete sensory stimuli, performances related to the judgment of durations, the mechanism of the attentional process mobilizes other conceptual models that gravitate mainly around the internal clock model and, in particular, the striatal beat frequency model which propose also neurobiological explanations (Matell & Meck, 2004). In this work, we aimed at understanding the role of the Amygdalo-nigro-striatal (ANS) circuit in the development of the attentional process in associative learning oriented towards discrete and temporal sensory stimuli in the rat. We also aimed at examining the role of this circuit in the evolution of the attentional process after over-training permitting the development of habits. In order to achieve this objective, we compared performance of rats with cross-lesion by altering the CeA in one hemisphere and the nigro-striatal circuit in the other hemisphere (Amygdalo-nigro-striatal disconnection; Contra group) to rats with lesions in the same hemisphere (CeA and nigro-striatal circuit: group Ipsi). A third group was submitted to bilateral lesions of the CeA (Amy group). A control group had pseudo lesions (groupe Sham).Through our three experimental groups (Contra, Ipsi and Amy) and the control group (Sham), we have shown the involvement of the CeA in the modulation of the attentional process when a novelty was introduced in the experimental situation (surprise) both in the presence of an appetitive discrete sensory stimulus and of a temporal stimulus in an aversive context. We have also shown that the ANS circuit is involved in habit formation and that there is probably a differential effect between the posterior and anterior part of the CeA. Our work also highlighted the implication of the nigro-striatal circuit in temporal discrimination and of the ANS circuit in the attentional treatment in temporal perception tasks, this effect being different depending on whether the discrimination concerns short or long durations.

.

.

Dans cette thèse, nous proposons une amélioration de l'automatisation des preuves dans l'assistant de preuve Coq. Cette automatisation est obtenue en intégrant à Coq les procédures de décision pour la logique propositionnelle, l'égalité et l'arithmétique linéaire constituant le noyau du solveur SMT Alt-Ergo. Cette intégration est réalisée en utilisant la technique de preuve par réflexion, qui consiste à développer en Coq ces algorithmes et à prouver formellement leur correction de manière à les exécuter directement dans l'assistant de preuve. Comme les algorithmes formalisés en Coq sont exactement ceux utilisés dans le noyau d'Alt-Ergo, notre travail permet également d'augmenter considérablement la confiance que l'on peut avoir dans ce dernier. En particulier, il utilise un algorithme original de combinaison de l'égalité modulo une théorie, inspiré de la combinaison de Shostak et appelé CC(X), et dont la justification est relativement complexe.Notre développement Coq est utilisable sous la forme de tactiques qui permettent de valider automatiquement des formules combinant logique propositionnelle, égalité et arithmétique. Afin que ces tactiques soient le plus efficaces possibles, nous avons attaché une grande importance aux performances de notre implantation Coq, et en particulier à l'utilisation de structures de données efficaces courantes, dont nous proposons ici une bibliothèque. / In this thesis, we propose new automation capabilities for the Coq proof assistant. We obtain this mechanization via an integration into Coq of decision procedures for propositional logic, equality reasoning and linear arithmetic which make up the core of the Alt-Ergo SMT solver. This integration is achieved through the reflection technique, which consists in implementing and formally proving these algorithms in Coq in order to execute them directly in the proof assistant. Because the algorithms formalized in Coq are exactly those in use in Alt-Ergo's kernel, this work significantly increases our trust in the solver. In particular, it embeds an original algorithm for combining equality modulo theory reasoning, called CC(X) and inspired by the Shostak combination algorithm, and whose justification is quite complex. Our Coq implementation is available in the form of tactics which allow one to automatically solve formulae combining propositional logic, equality and arithmetic. In order to make these tactics as efficient as may be, we have taken special care with performance in our implementation, in particular through the use of classical efficient data structures, which we provide as a separate library.

L'automatisation de la numérisation est une étape indispensable au développement de la mesure tridimensionnelle, et ce, dans différents domaines :<br />- en milieu industriel, afin d'accélérer les procédures de contrôle de pièces,<br />- en archéologie et en biologie, pour l'étude de collections de plusieurs centaines voire milliers d'objets (dont l'acquisition est pour le moment impossible en raison du temps nécessaire, et donc du coût).<br />Dans ce mémoire, nous détaillons tout d'abord les différents systèmes d'acquisition et de positionnement existants, en détaillant les avantages et inconvénients de chaque système. Nous présentons ensuite la méthodologie mise en place pour guider l'opérateur dans ces choix ainsi que l'outil d'aide mis en place afin de formaliser cette méthodologie. Puis nous argumenterons de la nécessité de l'automatisation de la numérisation 3D en illustrant les limites et les contraintes des solutions actuellement en place. Des exemples d'application de la méthodologie sont décrits à travers différentes études de cas, mettant en évidence le temps d'intervention de l'opérateur. Ensuite, les méthodes d'automatisation de l'acquisition existantes sont décrites, en expliquant leurs limites face à notre problématique. Deux méthodes sont ensuite proposées : la première définit une planification de vues hors-ligne à partir d'un modèle de référence tandis que la seconde calcule la meilleure position suivante sans aucune information a priori sur l'objet. Ces deux méthodes permettent une numérisation complète d'un objet sans intervention d'un opérateur. Afin de tester ces méthodes, un environnement de simulation a été implémenté, ainsi qu'un prototype. Enfin, les résultats obtenus sont présentés et comparés à une numérisation manuelle.

Cette thèse s'intéresse à la conception de systèmes complexes d'automatisation sûrs de fonctionnement dont l'évaluation est basée sur des scénarios. Pour déterminer un système optimal, il est important de disposer d'outils de modélisation et d'évaluation rapides ainsi que des algorithmes d'optimisation adaptés au sein d'une méthodologie globale de conception. Cette méthodologie doit également permettre d'étudier l'impact des défaillances sur le comportement final du système contrôlé. Dans ce cadre, la détermination d'un architecture matérielle, son optimisation vis-à-vis de critères comme la longueur minimale des scénarios et le nombre de combinaisons de scénarios sont considérés. Nous proposons une modélisation fonctionnelle et dysfonctionnelle utilisant les scénarios de modes de défaillances. Le niveau de détail considéré est suffisamment fin pour décrire différentes possibilités d'agencements des composants utilisables ainsi que plusieurs types de composants. Si la modélisation fonctionnelle est facile à appréhender, la modélisation dysfonctionnelle tenant compte des scénarios est plus difficile. Afin de répondre à ce problème, nous proposons un modèle graphique baptisé "Arbre de défaillances multiples amélioré" permettant de modéliser, à l'aide d'opérateurs temporels et de relations entre modes de défaillances, ce comportement dysfonctionnel. L'application de cette méthodologie à un système de ferroutage est présentée. Les résultats obtenus pour les fonctionnalités liées au problème de l'incendie et du désarrimage sont comparés avec une méthode classique d'évaluation afin de montrer l'efficacité de l'approche proposée. L'intégration de ces travaux dans un logiciel dédié à la conception de systèmes d'automatisation (plate forme ALoCSyS : Atelier Logiciel de Conception de Systèmes Sûrs) est décrite.

Thèse doctorat : Automatique, Traitement du signal, Génie Informatique : Nancy 1 : 2004. / Titre provenant de l'écran-titre.

Thèse (D. en informatique cognitive)--Université du Québec à Montréal, 2005. / En tête du titre: Université du Québec à Montréal. Bibliogr.: f. [172]-186. Publié aussi en version électronique.

Th. doct.-ing.--Lille 1, 1979. N°: 229.

Au cours des dernières années, l’automatisation en bactériologie clinique est devenue très importante du fait de l’augmentation constante du nombre d’échantillons mais nécessite tout de même des améliorations. Une revue a été rédigée pour présenter les nouveaux challenges et opportunités dans la surveillance et la détection des bactéries multi-résistantes. Premièrement nous avons testé de nouveaux outils technologiques innovants permettant la lecture plus précoce des antibiogrammes grâce à des scanners de haute résolution d’images: scanner Advencis Bio-System Incubator et le Scan® 1200 et de réaliser l’ensemencement des antibiogrammes en automatique sur un automate déjà existant le PREVI® Isola (bioMérieux, Marcy l’Etoile, France). Dans un second temps, une analyse rétrospective de la résistance aux antibiotiques observés sur l’hôpital la Timone à Marseille a été réalisé entre 2014 et 2016. Nous avons développer un logiciel d’interprétation automatique des phénotypes basé sur la reconnaissance d’images pour lequel un brevet a été rédigé : le logiciel « ANTI-LOGIC ». Le but de notre troisième travail a été de participer au développement d’une PCR en temps réel permettant de détecter le gène mcr-1. Puis, nous avons travaillé sur des souches multi-résistantes afin de tester un panel constitué de 29 à 32 antibiotiques. Pour la détection des souches résistantes à la colistine, un milieu de culture sélectif a été mis au point et nous avons essayé de trouver une alternative thérapeutique par l’étude de combinaisons d’anciens antibiotiques (colistine-sulfadiazine) pour le traitement et la décolonisation avant greffe fécale de patients infectés ou colonisés par des BMR. / In the last few years, automation in clinical microbiology has become very important due to the constant increase of samples but they need to be improved. A review of the literature was performed to expose the new challenges and the new opportunities in the surveillance and the detection of multi-drug resistance bacteria.For that purpose, we conduct a thorough search to test new innovative technological tools for reading earlier AST with high-resolution image scanner: Advencis Bio-System Incubator and the Scan® 1200 and to carry out the automatic seeding of AST with the PREVI® Isola system (bioMérieux, Marcy l’Etoile, France). In a second step, the retrospective analysis of antibiotic resistance and phenotypes observed at La Timone hospital in Marseille was carried out between 2014 and 2016. We have developped a new software for the automatic interpretation of phenotypes based on image recognition protected by a patent: the "ANTI-LOGIC" software. The aim of our third work was to participate on the development of a real-time PCR to detect the mcr-1 gene. We then worked on multi-resistant strains with Gram-negative bacteria, we have tested a large panel of 29-32 antibiotics to see if we are in a therapeutic stalemate. For the detection of colistin resistant strains, a selective culture medium has been developed. In order to finish this part, with the appearance of colistin-resistant strains, we tried to find a therapeutic alternative by studying combinations of old antibiotics (colistin-sulfadiazine) for the treatment and decolonization before faecal transplantation of patients infected or colonized by multi-resistant bacteria