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.

翻译：我们提出了一种在自动化推理课程中利用 Isabelle 证明助手测试学生学习成果的方法。该方法既能检验学生在多种逻辑证明系统中对形式化证明的总体理解，也能针对其在 Isabelle/HOL 高阶逻辑中证明能力的掌握程度进行测试。使用 Isabelle 可实现考试大部分内容的近乎全自动评分。我们通过若干示例问题阐释该方法，并逐一论证所选用问题类型能够有效衡量预期学习成果。最后，我们讨论了将该方法应用于自动化推理课程考试的实践经验，并提出了未来潜在的研究方向。