Logic theory

Ects : 5

Enseignant responsable :

Volume horaire : 36

Description du contenu de l'enseignement :

  • Revision of fundamental concepts of classical logic (propositional and first-order logic) that will be necessary for this course
  • Proofs of soundness and completeness of propositional and first-order logic
  • Decidability of propositional logic
  • Undecidability of first-order logic
  • Gödel’s incompleteness theorems (without proofs)
  • Modal logic: main systems and proofs using tableaux method
  • Formal verification by model-checking:
    • Linear-time Temporal Logic (LTL)
    • Computation Tree Logic (CTL)

Pré-requis recommandés :

Classical logic (propositional and first-order)

Compétence à acquérir :

In the first part of the course, students will learn some key results in classical logic and logical metatheory: soundness, completeness and (un)decidability of classical logic.

The second part of the course will focus on some non-classical logics, namely modal logic and temporal logics. Temporal logics will be used in formal verification by model-checking (the process to verify the correctness of computer systems concerning some specified behaviour).

Mode de contrôle des connaissances :

Written exam