Le développement de nouveaux systèmes de preuve, de formats de preuve améliorés et de méthodes de recherche de preuves constitue l’un des objectifs les plus fondamentaux de la logique. Mais qu’est-ce qu’une preuve ? Comment comparer des preuves (en fonction de la taille, de la structure, de la simplicité des arguments, etc.) ? Comment peut-on trouver une preuve de manière efficace ? Comment peut-elle être utilisée ? Les logiciens issus de différentes communautés proposent généralement des réponses différentes à ces questions. Leurs principes peuvent relever du savoir tacite au sein de leur propre communauté, tout en restant largement méconnus en dehors de celle-ci.
Le débat sur l’importance des preuves et sur les critères permettant d’en évaluer la qualité remonte à une tradition ancienne, sans doute aussi ancienne que la logique elle-même. À l’ère moderne, on peut citer par exemple l’opinion de Poincaré selon laquelle « une collection de faits n’est pas plus une science qu’un tas de pierres n’est une maison », le 24ème problème non publié de Hilbert qui pose la question des critères pour juger de la simplicité des preuves, ou encore le programme d’« unwinding » des preuves de Kreisel, avec sa question : « que savons-nous de plus, lorsque nous avons démontré un théorème, qu’il est vrai ? ». Avec la multiplicité actuelle des outils de déduction générant des preuves, des systèmes de preuve et des applications pratiques des preuves, ce débat est plus pertinent et animé que jamais. Il semble toutefois malheureusement fragmenté entre de nombreuses communautés, qui n’ont que très peu l’opportunité d’échanger.
La thématique de l’équipe est centrée sur la notion de preuve, ses utilisations comme support d’interactions (entre outils ou avec l’humain) et ses applications, en particulier dans les domaines de la sûreté logicielle et de l’intelligence artificielle, notamment du traitement automatique du langage naturel (TALN).
Permanents
Richard Moot, Chargé de recherche, CNRS
Simon Robillard, Maître de conférences, UM
David Delahaye, Professeur des universités, UM
Doctorants
Maximos Skandalis, CNRS
Loic Allegre, UM
Romain Sidhoum, UM
Autres personnels
Vincent Blazy, ATER, UM
Clemence Gerardin, CDD Ingénieur-Technicien, UM
Christian Retoré, Invité longue durée Eméritat, UM
L’équipe contribue à la théorie de la démonstration, en étudiant des questions telles que la sémantique des preuves, la correction et la complétude de systèmes de preuves, en développant des cadres théoriques permettant de connecter ou de comparer différents systèmes de preuves, et en élaborant des algorithmes de recherche de preuves pour ces systèmes. L’équipe a aussi vocation à mettre en pratique ses connaissances pour produire des techniques et des outils, notamment dans les domaines de la vérification de programmes, des langages de programmation et du TALN, avec en particulier des outils de déduction automatique, des outils de preuve interactive, de typage de programmes, et des outils d’analyse syntaxique et sémantique pour le langage naturel.
Ces recherches concernent diverses logiques, y compris la logique du premier ordre et la logique d’ordre supérieur (classique ou intuitionniste), les théories des types, les logiques modales, ou encore la logique linéaire. En regroupant des spécialistes de ces différentes logiques, et en favorisant les échanges entre ceux-ci, l’équipe profite d’une expertise large et est capable de mobiliser les langages les plus adaptés (du point de vue de l’expressivité, de la décidabilité, des outils disponibles) aux différents champs d’application qu’elle se propose d’explorer.
L’équipe étudie particulièrement les preuves sous l’angle des interactions : interactions entre théorie de la démonstration et domaines d’application (particulièrement la vérification de programmes et le TALN), interactions entre preuves et humains (preuve interactive de théorèmes, argumentation formelle), interactions entre outils de recherche de preuves, interactions au sein des preuves elle-mêmes (logique dialogique, sémantique des jeux), ou encore modélisation logique de processus interactifs (logiques modales).
Dans le domaine de la vérification de programmes, l’équipe promeut la production de certificats de preuves par les outils de déduction automatique, afin de permettre une confiance accrue en ces outils, et une meilleure réutilisabilité des résultats qu’ils produisent. Par ailleurs l’équipe conçoit et implémente des systèmes de preuves adaptés au raisonnement en présence de quantificateurs et de théories (arithmétique, ensembles, types inductifs, etc.), ces deux éléments étant typiquement nécessaires pour spécifier et vérifier des logiciels.
L’équipe étudie les liens entre programmes et preuves (correspondance de Curry-Howard), ainsi que l’utilisation de système de preuves, en particulier des systèmes de typage, pour la conception de langages de programmation sûrs.
Dans le domaine de la linguistique informatique, la logique et en particulier la théorie de la démonstration interviennent à la fois pour la syntaxe et pour la sémantique du langage naturel. Dans la syntaxe du langage naturel, la recherche de la démonstration correspond à l’analyse syntaxique (parsing-as-deduction). Les logiques utilisées pour la syntaxe (calcul de Lambek, fragments de la logique linéaire) sont généralement décidables, et on peut utiliser des prouveurs pour calculer les significations des phrases. L’équipe s’intéresse à la production de prouveurs pour ces logiques, mais aussi à l’étude de la structure des démonstrations des logiques adaptées au développement de grammaires.
Dans la sémantique du langage naturel, le sens est représenté dans une logique plus expressive : la logique du premier ordre ou d’ordre supérieur, étendue avec des opérateurs modaux. L’une des questions clés de la sémantique du langage naturel est la suivante : étant donnée une représentation logique de la signification de deux textes, quelle est la relation logique entre eux ? L’un implique-t-il l’autre ? Se contredisent-ils ? Comme pour la syntaxe du langage naturel, l’équipe utilisera et développera des prouveurs de théorèmes pour répondre à ces questions.