Menu Fermer

Logiques

Christian RETORE
Animateur

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, GRAPHIK, MAREL, SMILE et TEXTE.

Elles collaborent au-delà du LIRMM, localement avec le laboratoire IMAG (Montpellier), au niveau national avec les laboratoires :

Certains membres de l’axe participent au :

A l’étranger, des collaborations existent avec :

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.