Logique propositionnelle

- Syntaxe formelle de la logique des propositions : symboles, connecteurs, formules bien formées, arborescences syntaxiques, formes normales et clausales

- Sémantique de la logique des propositions : interprétation, modèle, tables de vérité, satisfiabilité, validité, équivalence sémantique, conséquence logique

- Modélisation : formalisation de problèmes en logique propositionnelle, limite d’expressivité de la logique propositionnelle

- Preuve formelle : séquents, règles d’inférences, axiomes, théorèmes, système LK, méthode de résolution

- Correction et complétude d’un système vis-à-vis d’une sémantique : preuve de correction et de la complétude du LK et de la méthode de résolution (réduit au cas propositionnel)

- Correspondance de Curry-Howard

- Introduction à la logique du premier ordre (calcul des prédicats) sans symbole de fonction