Archive 2022
Prérequissuivre le cours preuves-programmes : outils classiques en parallèle de ce cours constituera un complément judicieux.
Validationexamen
EnseignantAlexis Saurin et Thomas Colcombet
Horaires hebdomadaires 4 h CM
Années Master Logique Mathématique et Fondements de l'Informatique

Syllabus

Ce cours étudiera sous différents aspects la notion de second-ordre en logique et étudiera les logiques à points-fixes. On abordera notamment différentes applications informatiques de ces formalismes logiques à l'étude des langages formels sur les mots et les arbres et à l'étude des langages de programmation.

Sommaire

Partie 1: Logique et arithmétique du second-ordre, système F

-Syntaxe de la logique du second-ordre, déduction naturelle du second-ordre, théories et fragments particuliers (PA2, HA2, MSO, F, ...).

-Modèles du second-ordre: modèles pleins et modèles de Henkin, complétude au second-ordre.

-Preuves et programmes: extension de la correspondance de Curry-Howard (second-ordre et polymorphisme) et étude du système F (définition, représentation des types de données, théorèmes de normalisation (candidats de réductibilité de Girard, réalisabilité), fonctions représentables dans F).

Partie 2: Logique du second-ordre monadique

-Définitions, rappels et compléments sur la théorie des automates.

-Décidabilité sur les mots (Elgott-Büchi-Trakhtenbrot); liens avec les automates et les monoïdes.

-Le premier-ordre dans le second-ordre (théorème de Schützenberger).

-Décidabilité sur les structures ressemblant à des arbres (théorème de Courcelle) et les limites structurelles à la décidabilité (théorème de Seese).

-La méthode compositionnelle de Feferman-Vaught et Shelah.

-La théorie sur les mots infinis (Büchi, Safra).

-La théorie sur les arbres infinis et liens avec la théorie des jeux (Rabin, Gurevitch et Harrington).

Partie 3: Plus petits et plus grands points fixes en logique

-Quelques résultats sur les points-fixes.

-Syntaxes et sémantiques des logiques avec plus petits et plus grands points-fixes (définitions inductives à la Martin-Löf, mu-calcul pour les logiques classique, intuitionniste et modale).

-Systèmes de déduction pour les logiques à points-fixes: induction à la Park, règle Omega, preuves circulaires.

-Relations avec les automates, avec la logique du second-ordre monadique.

-Complétude du mu-calcul et autres résultats.

Bibliographie

  • Rudiments of mu-calculus, A. Arnold and D. Niwinski
  • Proofs and Types, JY Girard, P Taylor, Y Lafont
  • Proof-theory and Logical complexity, JY Girard -Lambda-calculus and models, JL Krivine
  • Proof Theory, Gaisi Takeuti
  • Survey of Wolfgang Thomas, Languages, Automata and Logic
  • Automata toolbox book https://www.mimuw.edu.pl/~bojan/papers/toolbox.pdf