On Exams with the Isabelle Proof Assistant

At the Technical University of Denmark, we currently teach a MSc level course on automated reasoning using the Isabelle proof assistant [11] as our main tool. The course is a 5 ECTS optional course and the homepage is here: https://courses.compute.dtu.dk/02256/ The course is an introduction to automatic and interactive theorem proving, and Isabelle is used to formalize almost all of the concepts we introduce during the course. We have developed a number of external tools to allow us to teach basic proofs in natural deduction and sequent calculus while slowly progressing towards showing students the full power of Isabelle. The learning objectives of the course are as follows: 1. explain the basic concepts introduced in the course 2. express mathematical theorems and properties of IT systems formally 3. master the natural deduction proof system 4. relate first-order logic, higher-order logic and type theory 5. construct formal proofs in the procedural style and in the declarative style 6. use automatic and interactive computer systems for automated reasoning 7. evaluate the trustworthiness of proof assistants and related tools 8. communicate solutions to problems in a clear and precise manner We expect students to already know some logic and to be relatively proficient in functional programming before starting the course. Additionally, we expect students to have some basic knowledge of artificial intelligence algorithms for deduction. Our undergraduate program in computer science and engineering, which many of our students have completed, contains several courses that introduce students to these topics.