Une introduction à la logique informatique, avec pour programme :

  • Calcul propositionnel : syntaxe et sémantique. Tables de vérité, tautologies. Formes normales, forme clausale. Modélisation, solveurs SAT, recherche de modèles, algorithme DPLL. Recherche de preuve, calcul des séquents.
  • Logique du premier ordre : syntaxe et sémantique. Formes normales, skolémisation. Modélisation, solveurs SMT. Recherche de preuve, calcul des séquents.

Ce cours de logique 2019­—2020 combine les cours « outils logiques » et « logique » des années précédentes.