In this advanced course on computational logic we plan to cover the following topics:
- Boolean Logic
- Set Theory
- Computation Theory
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 an oral exam and homework (including Coq developments).
Lectures are 12.15-13.45 on Tuesdays and Thursdays. The first lecture is on October 25, and the last lecture is on January 12. See the timetable for more information.
Lecture Notes
- This year: Boolean logic, set theory
- Lecture notes ICL from SS 2014
- Lecture notes CL II from WS 2014