In this advanced course on computational logic we plan to cover the following topics:
- Boolean Logic
- Set Theory
- Modal Logic
- Finitary Sets
- Computation Theory
- Substitution Algebra
The topics will be discussed from a constructive and type theoretic perspective. Students are assumed to be familiar with the formalization of mathematical theories in the proof assistant Coq as covered in the course Introduction to Computational Logic.
Credit and grades will be based on two oral exams and homework (including Coq developments).
Lectures are 12.15-13.45 on Wednesday and Friday. See the timetable for more information.