# On Exams with the Isabelle Proof Assistant

arXiv: https://arxiv.org/abs/2303.05866 · HTML: https://mlsanity.com/paper/2303.05866/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 4 of its 18 references that are in the map.
- First posted on arXiv 10 Mar 2023.

## Builds on (most cited first, 4 of 4)

- [SeCaV: A Sequent Calculus Verifier in Isabelle/HOL](https://mlsanity.com/paper/2204.03884/) (2022)
- [Natural Deduction Assistant (NaDeA)](https://mlsanity.com/paper/1904.00618/) (2019)
- [Isabelle/HOL as a Meta-Language for Teaching Logic](https://mlsanity.com/paper/2010.16014/) (2020)
- [Teaching Intuitionistic and Classical Propositional Logic Using Isabelle](https://mlsanity.com/paper/2202.03567/) (2022)

## Built on by (most cited first, 1 of 1)

- [Teaching Higher-Order Logic Using Isabelle](https://mlsanity.com/paper/2404.05458/) (2024)

## Abstract (arXiv)

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.