Ects : 5

Enseignant responsable :

• GABRIELLA PIGOZZI

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