Logiques, graphes et langages
Responsable : Sylvain Lombardy.

Présentation générale

Les méthodes formelles considérées sont principalement celles de la Théorie des Langages Formels et de la Logique.

Les concepts fondamentaux de la théorie des langages que sont les grammaires, les automates, la reconnaissabilité exprimée en termes de congruences, et qui ont été développés tout d'abord pour les mots et les termes finis et infinis, sont appliqués à d'autres objets tels que les ordres partiels et les graphes, et à d'autres structures mathématiques que le monoïde et l'algèbre libre, telles que le groupe libre et à différents types de semi-groupes. Les objectifs généraux sont toujours de décrire des familles d'objets par des moyens finis et de décider diverses propriétés d'objets et/ou d'ensembles infinis donnés par leurs descriptions finies.

La logique, qui est essentielle dans les travaux de l'équipe Méthodes Formelles sur la vérification et la linguistique informatique, intervient ici à plusieurs titres :

  • la logique du second-ordre monadique est devenue un outil incontournable en théorie des langages : ceci est dû à son équivalence avec la notion d'automate fini sur les mots et les termes finis ou infinis ; elle est particulièrement importante en théorie des grammaires de graphes car elle remplace les automates finis : en effet, cette notion n'existe pas pour les graphes, sauf dans des cas très particuliers ;
  • les problèmes de graphes spécifiés dans ce langage sont de complexités paramétrées respectivement cubique et linéaire par rapport aux largeurs de clique (clique width) et arborescente (tree width) ; cela justifie une relecture des constructions fondamentales de la théorie des graphes en vue de leur expression dans ce langage, et par ailleurs, la construction et l'implémentation des algorithmes issus de la théorie ;
  • le calcul des constructions (lambda-calcul d'ordre supérieur) permet de formaliser des preuves mathématiques, éventuellement très difficiles telles que celle du théorème des 4 couleurs, et de les vérifier ; les assistants de preuve fournissent une aide à la conception, à l'écriture et à la vérification de telles preuves.

Ces différentes directions de recherche sont présentées plus en détail dans les pages annexes :

Page mise à jour le 08/02/2016 à 09:33