Presentation of the fundamental principles and formal tools at the basis of all methods of design, verification and implementation of computer systems. Thus, the fundamental notions of mathematical logic and automatic demonstration at the basis of all these techniques of modeling and verification of computer systems are addressed. Classical logic formalisms such as propositional logic and first order logic, but also non-classical logic formalisms such as modal logic (widely used for multi-agent systems and data representation) are presented.

**Teaching time performed:** 6 hours of lectures, 3 hours of tutorials, and 3 hours of practical classes in Coq.

Part of the teaching team for the school year 2021-2022 and 2022-2023.

**Instructors:** Marc Aiguier, Pascale Le Gall, and Fabrice Popineau.

**Student level:** Third year (~M2/MSc).

Syllabus

- Propositional logic:
- Syntax, semantics, and basics results (compacity, NP-completeness)
- Calculus (Hilbert-style, sequent calculus) and semantic tableaux

- First-order logic:
- Syntax, semantics, and basics results (Löwenheim–Skolem theorem)
- Calculus (Hilbert-style, LK sequent calculus, resolution)

- Modal logic:
- Syntax, semantics, and basics results (finite models)
- Calculus (Hilbert-style, LK sequent calculus, resolution)

- Coq practical session