| Crédit : 5 ECTS |
| Langue du cours : anglais
|
|
|
|
Volume horaire
- CM :
36 h
- Volume horaire global (hors stage) :
36 h
Compétences à 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).
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)
Mode de contrôle des connaissances
Written exam
Pré-requis recommandés
Classical logic (propositional and first-order)
Enseignant responsable
GABRIELLA PIGOZZI