Presentation
Computer science has its roots in mathematical logic, in the 1930s: can we decide mechanically on the validity of a statement? what can we calculate? how to represent data by integers? Today, these fundamental questions of computability are still relevant, and new aspects of logic are being developed, in particular for the security of programs and cyber-physical systems, or so that agents and robots with artificial intelligence can reason correctly.
At LIRMM, members of several teams are pursuing fundamental research on the subject, for example on computability, while exploring applications of logic that have appeared more or less recently, such as program proofs, knowledge representation, argumentation, or the logical analysis of natural language.
Logic issues studied at LIRMM
Among the logic issues that are a source of interaction between LIRMM members, we mention :
- Proof finding in classical logic and program verification.
- Decidable fragments of classical logic, description logics, and knowledge representation.
- Logic and argumentation: Dung-like argumentation and partial proofs, dialogical logic.
- Proof finding in linear logic, with its applications to natural language semantics, or Petri nets.
- First and second order quantification in classical, intuitionistic, modal, linear logics and non-standard quantifiers and its expression in natural language reasoning (UM Quanti 2017 project)
- Computability, constructible and ordinal admissible sets.
- Logic and parametric complexity, finite models, monadic second order logic.
The LIRMM teams involved in these themes are: ALGCO, ESCAPE, BOREAL, MAREL, SMILE and TEXTE.
They collaborate beyond LIRMM, locally with the IMAG laboratory (Montpellier), and nationally with the :
- I2M (Marseille),
- IJN (CNRS-EHESS-ENS),
- IRIF (University of Paris),
- LaBRI (Bordeaux),
- Inria (EPC Partout), Deducteam et Valda.
Some members of the axis participate in the:
- GDR international logique linéaire,
- GDR informatique mathématique (GT Scalp et HLT),
- GDR philosophie des mathématiques
Abroad, collaborations exist with:
- ILLC Amsterdam (Netherlands),
- TU Dresden (Germany),
- University of Berkeley (CA, USA),
- TU Wien (Austria),
- Università Roma tre (Italy).
The members of the Logic Axis regularly organise study days, including the UNESCO Logic Day every 14 January since 2019, an international workshop on epsilon and tau quantifiers, days on quantification, days on linear logic, formal proofs, decidable fragments of first-order logic.
More detailed information can be found here.