During this course, students will learn

- Propositional logic proof theory and semantics
- First-order logic proof theory and semantics
- Model checking: Linear-Temporal Logic, Computation Tree Logic and applications
- Proof terms and lambda calculus
- Proofs as programs, functional languages and type checking
- Sequent calculus and automated proof construction
- Foundations of Logic Programming, Prolog