Logic theory

ECTS : 5

Volume horaire : 36

Description du contenu de l'enseignement :

• Revision of fundamental concepts of classical logic (propositional and first-order logic)
• Soundness and completeness of propositional and first-order logic
• Decidability of propositional logic
• Undecidability of first-order logic
• Gödel’s incompleteness theorems (no proofs)
• Formal verification by model-checking:
  • Linear-time Temporal Logic (LTL)
  • Computation Tree Logic (CTL)

Compétence à acquérir :

In the first part of the course, students will learn some key results in classical logic and logical metatheory.

The second part of the course will focus on formal verification to verify the correctness of computer systems concerning some specified behaviour.

Mode de contrôle des connaissances :

Written exam