On Exams with the Isabelle Proof Assistant
This addresses the problem of efficient and reliable assessment in automated reasoning education, though it is incremental as it applies existing tools to a specific educational context.
The authors developed an approach for testing student learning outcomes in automated reasoning courses using the Isabelle proof assistant, enabling almost automatic grading of large parts of exams. They validated this through example problems and discussed experiences from a course exam.
We present an approach for testing student learning outcomes in a course on automated reasoning using the Isabelle proof assistant. The approach allows us to test both general understanding of formal proofs in various logical proof systems and understanding of proofs in the higher-order logic of Isabelle/HOL in particular. The use of Isabelle enables almost automatic grading of large parts of the exam. We explain our approach through a number of example problems, and explain why we believe that each of the kinds of problems we have selected are adequate measures of our intended learning outcomes. Finally, we discuss our experiences using the approach for the exam of a course on automated reasoning and suggest potential future work.