Menu Fermer

Logiques

Christian RETORE
Animateur
icône enveloppe
Contact

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.

visuel logique

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 dans diverses logiques et ses applications en informatique : vérification de programmes, preuves de satisfiabilité et de cohérence pour la représentation des connaissances ;
  • L’étude de fragments décidables de la logique classique, logiques de description, logique modales, et représentation des connaissances.
  • Logique et modèle de l’argumentation : argumentation à la Dung, logique dialogique ; applications en didactique des mathématiques et en droit ;
  • La quantification du premier et du second ordre dans des logiques classiques, intuitionnistes, modales, linéaires et les quantificateurs non standard et son expression en langage naturel
  • 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, COCONUT, ESCAPE, BOREAL, 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 :

Chaque année, les membres de l’axe transverse « Logiques » organisent la journée UNESCO de la logique chaque 14 janvier depuis 2019, ainsi  des journées d’études, sur des thèmes variés (graphes et logique, fragment décidable de la logique du premier ordre, preuves formelles, logique modale, …) rassemblant au moins deux équipes. Quelques exemples sont donnés ci-dessous, et la liste complète de ces événements se trouve  ici.

Focus :

Quelques événements organisés dans le cadre de notre axe transverse « LOGIQUES » du LIRMM :