On Exams with the Isabelle Proof Assistant

Frederik Krogsdal Jacobsen, Jørgen Villadsen
3/10/2023
cs.LOcs.AI

No confident code implementation found for this paper.

Abstract

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.

View on arXivView PDF

Code Implementations

No confident code match yet

We couldn't find an author-owned or strongly-evidenced community implementation for this paper. Any repos shown below are weak matches — verify before relying on them.

No code implementations found yet.

Know of an implementation? Let us know in the comments below!

Similar Papers

Learning Guided Automated Reasoning: A Brief Survey

82% match2024

Teaching Higher-Order Logic Using Isabelle

82% match2024

Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verification

80% match1 repo312024

Trustworthy Formal Natural Language Specifications

80% match2023

Mathematical Proof Assistants for Teaching Logic: The LogiKEy Methodology

80% match2026

Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification

79% match1 repo42024

Cite this paper

@article{jacobsen2023exams,
  title  = {On Exams with the Isabelle Proof Assistant},
  author = {Frederik Krogsdal Jacobsen and Jørgen Villadsen},
  year   = {2023},
  eprint = {2303.05866},
  archivePrefix = {arXiv},
  url    = {http://arxiv.org/abs/2303.05866v1}
}

Add a badge to your README

Shows whether official code is linked for this paper.

Code of Paper badge
[![Code of Paper](https://codeofpaper.com/badge/2303.05866.svg)](https://codeofpaper.com/paper/2303.05866)

Discussion