Présentation
L’informatique a pris sa source dans la logique mathématique, dans les années 1930 : peut-on décider mécaniquement de la validité d’un énoncé ? que peut-on calculer ? comment représenter des données par des entiers ? Aujourd’hui ces questions fondamentales de calculabilité restent d’actualité, et de nouveaux aspects de la logique se développent, notamment pour la sécurité des programmes et des systèmes cyber-physiques, ou pour que les agents et robots dotés d’une intelligence artificielle puissent raisonner correctement.
Au LIRMM, les membres de plusieurs équipes poursuivent des recherches fondamentales sur le sujet, par exemple sur la calculabilité, tout en explorant des applications de la logique apparues plus ou moins récemment, comme les preuves de programmes, la représentation des connaissances, l’argumentation, ou l’analyse logique du langage naturel.
Questions de logique étudiées au LIRMM
Parmi les questions de logique qui sont source d’interactions entre les membres du LIRMM, nous mentionnons :
- La recherche de preuve en logique classique et la vérification de programme.
- Des fragments décidables de la logique classique, logiques de description, et représentation des connaissances.
- Logique et argumentation : argumentation à la Dung et preuves partielles, logique dialogique.
- La recherche de preuve en logique linéaire, avec ses applications à la sémantique du langage naturel, ou aux réseaux de Petri.
- La quantification du premier et du second ordre dans des logiques classiques, intuitionnistes, modales, linéaires et les quantificateurs non standard et son expression dans le raisonnement en langage naturel (projet UM Quanti 2017)
- Calculabilité, ensembles constructibles et ordinaux admissibles.
- Logique et complexité paramétrique, modèles finis, logique monadique du second ordre.
Les équipes du LIRMM impliquées sur ces thématiques sont ALGCO, ESCAPE, BOREAL, MAREL, SMILE et TEXTE.
Elles collaborent au-delà du LIRMM, localement avec le laboratoire IMAG (Montpellier), au niveau national avec les laboratoires :
- I2M (Marseille),
- IJN (CNRS-EHESS-ENS),
- IRIF (Université de Paris),
- LaBRI (Bordeaux),
- Inria (EPC Partout), Deducteam et Valda.
Certains membres de l’axe participent au :
- GDR international logique linéaire,
- GDR informatique mathématique (GT Scalp et HLT),
- GDR philosophie des mathématiques
A l’étranger, des collaborations existent avec :
- ILLC Amsterdam (Pays-Bas),
- TU Dresden (Allemagne),
- University of Berkeley (CA, USA),
- TU Wien (Autriche),
- Università Roma tre (Italie).
Les membres de l’axe Logique organisent régulièrement des journées d’études, notamment la journée UNESCO de la logique chaque 14 janvier depuis 2019, un workshop international sur les quantificateurs epsilon et tau, des journées sur la quantification, des journées sur la logique linéaire, les preuves formelles, les fragments décidables de la logique du premier ordre.
Des informations plus détaillées se trouvent ici.Focus :
Journée Mondiale de la Logique 2023 – samedi 14 Janvier 2023 10:00-13:00
3 exposés :
- 10h Incomplétude et calculabilité Bruno DURAND (LIRMM, Univ Montpellier et CNRS)
- 11h Logique et langage : éléments d’une longue histoire Christian RETORÉ (LIRMM, Univ Montpellier et CNRS)
- 12h Sécurité des programmes et logique modale Davide CATTA (Telecom Paris, Institut Polytechnique de Paris)