Tableau d'honneur de la Faculté des études supérieures et postdoctorales, 2011-2012 / Une des questions incontournables qu'on se pose en théorie des langages est de savoir si une logique est décidable. Autrement dit, pour une logique donnée, on veut savoir s'il existe un algorithme qui détermine si un langage donné est exprimable dans cette logique. Depuis les travaux de Schützenberger, McNaughton et Papert sur la logique de premier ordre sur les mots, on reconnait l'importance de la théorie algébrique des langages pour résoudre ces questions de décidabilité. Un autre exemple historique est la caractérisation de Simon des langages testables par morceaux de mots par les monodes J -triviaux. On dit qu'un langage est testable par morceaux si on peut le définir par une combinaison booléenne d'expressions régulieres de la forme [symbol]. Ces langages sont exactement ceux qui sont définis par la clôture booléenne de [symbol] et le théorème de Simon engendre un algorithme qui en resout la décidabilité. Suite aux succès sur les mots, on a attaque les mêmes questions de décidabilité de logiques sur les langages de forêts, plus spéciquement sur les langages d'arbres. Dernièrement, Bojanczyk, Segoufin et Straubing ont pu démontrer un analogue du théorème de Simon pour les forêts. En effet, ils ont pu caractériser la clôture booléenne de [symbol], c'est-à-dire les langages testables par morceaux, en fonction d'une structure algébrique nommée algèbre de forêts. Ce mémoire est d'abord un état de l'art de la théorie algébrique des langages testables par morceaux. Entre autres, nous présentons le théorème de Simon sur les mots en passant par un résultat de Straubing et Thérien qui utilise la théorie des monodes partiellement ordonnés. Ensuite, nous étudions un pendant de ce résultat pour les algèbres de forêts. Finalement, nous règlons la décidabilité des langages de mots bien emboîtés testables par morceaux, une sous-classe des langages visiblement à pile. En efet, nous proposons un algorithme qui utilise le résultat de Bojanczyk, Segoufin et Straubing sur les langages de forêts.

L'œuvre logique d'Albert le Grand a été très peu étudiée jusqu'ici. Ses enseignements sur le problème fondamental du sujet de la logique, entre autres, n'ont suscité que quelques remarques et brèves études. Le peu qui a été fait semble d'ailleurs indiquer que cet oubli est pleinement justifié : le philosophe médiéval paraît incohérent et peu profond. Une étude de plus grande envergure, tenant compte de tous les textes de l'auteur sur ce sujet et de toutes les nuances dont le maître de Thomas d'Aquin est capable, met toutefois en lumière sa connaissance exceptionnelle de tous les aspects de cette difficile question. Plus important encore, elle nous procure une solution équilibrée, solide et fort éclairante pour qui tente de percer le corpus logique aristotélicien: le sujet de la logique se présente comme l'instrument rationnel, d'une part, et comme l'intention seconde (ou l'argument, ou l'expression linguistique), d'autre part.

Le présent mémoire propose une investigation approfondie de l’analyseur Alloy afin de juger son adaptabilité en tant que vérificateur de modèles. Dans un premier temps, l’étude dresse un tableau comparatif de six vérificateurs de modèles, incluant Alloy, afin de déterminer lequel d’entre eux est le plus apte à résoudre les problématiques de sécurité fonctionnelle posées par les systèmes d’information. En conclusion de cette première phase, Alloy émerge comme l’un des analyseurs les plus performants pour vérifier les modèles sur lesquels se fondent les systèmes d’information. Dans un second temps, et sur la base des problématiques rencontrées au cours de cette première phase, l’étude rapporte une série d’idiomes pour, d’une part, présenter une manière optimisée de spécifier des traces et, d’autre part, trouver des recours afin de contourner les limitations imposées par Alloy. À ces fins, le mémoire propose deux nouveaux cas d’espèce, ceux d’une cuisinière intelligente et d’une boîte noire, afin de déterminer si oui ou non l’analyseur est capable de gérer les systèmes dynamiques possédant de nombreuses entités avec autant d’efficacité que les systèmes qui en possèdent moins. En conclusion, le mémoire rapporte que Alloy est un bon outil pour vérifier des systèmes dynamiques mais que sa version récente, DynAlloy, peut être encore mieux adapté pour le faire puisque précisément conçu pour faire face aux spécificités de ce type de système. Le mémoire s’achève sur une présentation sommaire de ce dernier outil.

Ce mémoire présente l'étude d'une approche particulière des langages de programmation logico-fonctionnels, fondée sur la logique des clauses de Horn avec égalité. Nous définissons d'abord la syntaxe et la sémantique des programmes que nous considérons. La syntaxe est celle de la logique des clauses de Horn avec égalité. La sémantique est donnée par le plus petit e-modele de Herbrand associe a un programme. Nous nous intéressons ensuite au calcul dans ce langage. Nous proposons pour cela une nouvelle règle appelée sldei-resolution comme seule règle de calcul. Nous montrons sa cohérence, sa complétude ainsi que sa completude forte. La mise en œuvre de la règle sldei-resolution nécessite un algorithme de resolution d'équations. Nous étudions de tels algorithmes fondes sur la relation de surreduction, et améliorons ces algorithmes par l'utilisation de stratégies de surreduction. Cependant, ces stratégies ne sont pas complètes dans le cas général. Nous proposons alors des conditions suffisantes sur ces stratégies afin de préserver la complétude des algorithmes considérés. Nous caractérisons ensuite une classe de programmes, dits uniformes, pour lesquels l'utilisation de n'importe quelle stratégie de surreduction donne un algorithme complet de resolution d'équations. Nous donnons de plus une methode de vérification de l'uniformité d'un programme. Par ailleurs, nous proposons des conditions syntaxiques pour qu'un programme soit uniforme. Enfin, nous décrivons les principaux traits d'un langage de programmation fonde sur l'approche présentée dans ce mémoire, et l'implantation que nous avons réalisée

La logique linéaire (LL) permet de prendre naturellement en compte la notion de ressource. Elle est ainsi très expressive : le plus petit fragment propositionnel est déjà NP-complet alors que le plus grand est indécidable car on peut y simuler les modèles de calculs usuels comme les machines à registres. La décidabilité du fragment multiplicatif exponentiel de LL (MELL) est un problème ouvert. Cette thèse établit la complétude de la sémantique des phases semi-linéaire pour le fragment de Horn de MELL. La prouvabilité dans ce dernier est équivalente à l'accessibilité dans les réseaux de Pétri. Ce résultat constitue une première étape vers l'éventuelle décidabilité de MELL (conjecture de Y.Lafont). Le chapitre suivant développe le codage du problème des circuits hamiltoniens où la notion de choix (qui est ici naturellement traduite par les connecteurs additifs) est gérée multiplicativement. Ce procédé pourrait être étendu à l'étude d'autres problèmes de théorie des graphes. On obtient ainsi une nouvelle preuve de la NP-complétude du fragment multiplicatif de la logique linéaire. C'est un travail réalisé en commun avec T.Krantz. Enfin, on donne un critère de correction quadratique pour les réseaux de preuves de la logique non-commutative de P.Ruet (qui contient la logique linéaire et la logique linéaire cyclique). Il permet de plus de traiter les réseaux de preuve avec coupures.

Ce travail se situe dans le cadre des systèmes informatiques pour l'enseignement intégrant des capacités de raisonnement. Les exigences de ces EIAO (Environnement Interactif d'Apprentissage avec Ordinateur) sont à la fois d'ordre didactique et d'ordre informatique : exigence d'un contrat didactique à la sémantique claire et pré­cise; exigence d'une liberté maximale donnée à l'enseignant dans la formulation de ce contrat; exigence de capacités de déduction complètes; exigence de performances garantissant un niveau d'interactivité suffisant. Concrétement, nous avons conçu et réalisé le système TALC (Tuteur d'Aide Logique à la Construction) pour l'enseignement de la géométrie, dont l'objectif est de diagnostiquer la correction de la construction d'un apprenant vis-à-vis de la spécification d'une figure donnée par un enseignant. La définition du contrat didactique constitue le point central de notre travail. Notre point de vue est que son expression à l'aide de la logique du premier ordre est nécessaire à la fois pour obtenir une définition claire et pour fournir de bonnes explications à l'apprenant. Nous donnons ainsi une sémantique précise aux langages manipulés par le système : le langage logique LDL - à partir duquel est déterminé le diagnostic - et les langages d'interface. Nous présentons aussi les principes de la formulation de la théorie logique représentant les connaissances présupposées de l'élève. Nous établissons, par étapes de dérivation successives, l'expression logique de la correction d'une construction. Cette attitude est fructueuse. Elle nous a amenés à proposer le concept d'extension logique d'une formule par rapport à une autre, nécessaire pour prendre en compte des objets non décrits dans la spécification. Les perspectives ouvertes sont les suivantes : amélioration de la formulation du contrat didactique (par une meilleure définition de la négation), extension des langages d'interface, constitution de séquences didactiques, construction d'un modèle de l'apprenant à l'aide de techniques d'apprentissage et définition d'un langage d'expression des dialogues à tenir.

Le contexte général de mes travaux de recherche se situe dans le domaine de la représentation, modélisation puis combinaison des connaissances en milieu imprécis et vague, en particulier dans la théorie des sous-ensembles flous, d'une part, et dans la théorie des multi-ensembles, d'autre part. Dans ce contexte, nous nous attachons à concevoir des modèles ou outils linguistiques pour palier les problèmes d'imprécision. Notre travail s'est d'abord fondé sur la modulation, préservant la simplicité d'un espace de variables linguistiques de cardinalité assez faible mais sur lequel un large éventail de nuances peut être appliqué. Puis nous avons utilisé ces modèles et outils dans des contextes où l'expression de nuances est très importante, comme le *perceptual computing* dans le domaine de la classification des couleurs ou encore le jeu théâtral, et, plus récemment, pour la capture des intentions des programmeurs pour établir des politiques de contrôle et d'adaptation dynamique des architectures logicielles selon l'approche du calcul auto-régulé (*autonomic computing*).

Les logiques modales sont des logiques permettant la représentation et l'inférence de connaissances. La logique hybride est une extension de la logique modale de base contenant des nominaux, permettant de faire référence à un unique individu ou monde du modèle. Dans cette thèse nous présentons plusieurs algorithmes de tableaux pour logiques hybrides expressives. Nous présentons aussi une implémentation de ces calculs, et nous décrivons les tests de correction et de performance que nous avons effectués, ainsi que les outils les permettant. De plus, nous étudions en détail une famille particulière de logiques liée aux logiques hybrides : les logiques avec opérateurs de comptage. Nous étudions la complexité et la décidabilité de certains de ces langages.

Le raisonnement efficace dans une grande base de connaissance en logique de description est un défi actuel en raison des inférences "insurmontables", même pour des langages des logiques de description relativement inexpressives. En effet, la présence des axiomes dans la terminologie (TBox) est une des raisons importantes causant une augmentation exponentielle de la taille de l'espace de recherche explorée par les algorithmes d'inférence. Le raisonnement dans la logique de description (LD), c'est essentiellement le test de la relation de la subsomption entre les concepts. Par conséquent, on cherche toujours les expédients pour optimiser ce raisonnement. Des techniques d'optimisation pour améliorer la performance du raisonneur d'une LD se divisent donc naturellement en trois niveaux. Le premier est le niveau conceptuel considérant des techniques pour optimiser les structures d'axiomes dans la TBox. Le deuxième, le niveau algorithmique examinant des techniques pour réduire les exigences de stockage de l'algorithme de tableaux et pour optimiser le test de la relation de subsomption (satisfaisabilité). Le troisième, l'optimisation de requête cherchant des stratégies d'exécution optimales d'une requête d'interrogation dans une base de connaissances. Dans ce mémoire, nous avons étudié une approche de décomposition de l'ontologie s'appelant la "décomposition overlay" qui vise à un deux objectifs principaux : l'optimisation du raisonnement et la méthodologie de conception des ontologies. D'une part l'optimisation pour laquelle nous cherchons à diviser une ontologie dans un ensemble de sous ontologies dont chacune contient une partie de l'ensemble d'axiomes de l'ontologie originale permet d'obtenir ainsi une réduction relative du temps de raisonnement ; d'autre part la méthodologie de conception qui permet de remplacer une ontologie par un ensemble d'ontologies dans une organisation plus ou moins "optimale". Pour le premier objectif, la décomposition overlay d'une ontologie a comme résultat un ensemble de sous-ontologies regroupées dans une ontologie distribuée, appelée ontologie-décomposante (TBox-décomposante) et représentée par la logique de description distribuée. Intuitivement, le fait de pouvoir raisonner parallèlement sur ces sous-ontologies ayant chacune un espace de recherche réduit peut conduire à une réduction du temps relatif du raisonnement. Une propriété importante de cette ontologie est d'être interprétée dans le même domaine que l'ontologie originale. Ceci est une base qui nous suggère la proposition de deux algorithmes de raisonnement pour cette ontologie-décomposante. Concernant l'objectif de méthodologie de conception, nous introduisons deux méthodes de décomposition de l'ontologie reposant sur la décomposition heuristique des graphes. Une méthode repose sur la décomposition selon les séparateurs minimaux des graphes triangulaires et la seconde sur la décomposition selon la mesure des coupes normalisées des régions d'un graphe.

Cette note de synthèse rédigée en vue de soutenir une habilitation à diriger des recherches (HDR) a comme but de proposer une relecture de l'ensemble de travaux de recherche que je conduis depuis une quinzaine d'année sur l'articulation entre la logique et le raisonnement mathématique à la lumière de la théorie élémentaire des modèles de Tarski, qui joue ici le rôle de référence épistémologique pour les analyses didactiques. Une première partie présente les aspects de la théorie des modèles que j'ai retenu pour les études didactiques, ainsi qu'un exemple de l'utilisation de ce cadre pour repenser les questions de vérité, de validité, de nécessité et de certitude. La suite du document développe les analyses suivant trois axes : un retour sur les connecteurs logiques au-delà des tables de vérité ; un questionnement de différentes pratiques ordinaires dans la classe de mathématiques concernant la gestion des questions de quantification ; l'interprétation des énoncés mathématiques sous les angles syntaxique, sémantique et pragmatique. Ceci permet de réinterpréter un certain nombre d'erreurs classiques de logique ; de réduire la distance supposée entre logique de sens commun et logique mathématique et de s'interroger sur certains choix d'enseignement eu égards en particulier aux objectifs d'apprentissage visés en terme de rigueur.<br />Les résultats obtenus dans ce cadre théorique général permettent d'envisager un programme de recherche suivant deux axes complémentaires. Le premier axe concerne le développement des travaux visant à élucider le rôle que joue le formalisme logique dans l'élaboration des connaissances mathématiques au niveau de l'enseignement universitaire en lien avec la mise en œuvre d'ingénieries didactiques. Le second axe concerne la poursuite des recherches amorcées sur le croisement entre analyses didactiques et analyses dynamiques du discours dans la classe de mathématiques en mobilisant les ressources offertes par la sémantique logique.