Logiques et preuves

Acquérir les concepts et les techniques de modélisation et de construction de preuves au travers des logiques non-classiques utilisées en vue de modéliser et prouver des propriétés de programmes et de systèmes.

Sujets abordés

  • Logique classique et non-classiques.
  • Logique intuitionniste et logiques modales : sémantique à la Kripke, sémantique de Heyting, isomorphisme
  • de Curry Howard.
  • Théorie de la démonstration (déduction naturelle, calcul des séquents) et déduction automatique (tableaux, connexions, résolution). Lambda calculs associés (normalisation, types).
  • Logique linéaire : réseaux de preuve, sémantique et modélisation des ressources.
  • Logique d’ordre supérieur et du second ordre. Système F (types, forte normalisation, réductibilité).