On Exams with the Isabelle Proof Assistant

Frederik Krogsdal Jacobsen; Jørgen Villadsen

doi:10.4204/EPTCS.375.6

On Exams with the Isabelle Proof Assistant

Frederik Krogsdal Jacobsen, Jørgen Villadsen

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

69 Downloads (Pure)

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.

Original language	English
Title of host publication	Proceedings of the 11th International Workshop on Theorem Proving Components for Educational Software
Volume	375
Publisher	EPTCS
Publication date	2023
Pages	63-76
DOIs	https://doi.org/10.4204/EPTCS.375.6
Publication status	Published - 2023
Event	11^th International Workshop on Theorem Proving Components for Educational Software - Haifa, Israel Duration: 11 Aug 2022 → 12 Aug 2022

Workshop

Workshop	11^th International Workshop on Theorem Proving Components for Educational Software
Country/Territory	Israel
City	Haifa
Period	11/08/2022 → 12/08/2022

Access to Document

10.4204/EPTCS.375.6Licence: CC BY

FulltextFinal published version, 832 KBLicence: CC BY

OpenUrl availability

Full text

Cite this

@inproceedings{e4883484af814b3f988b7da9b5e2c1d0,

title = "On Exams with the Isabelle Proof Assistant",

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.",

author = "Jacobsen, {Frederik Krogsdal} and J{\o}rgen Villadsen",

year = "2023",

doi = "10.4204/EPTCS.375.6",

language = "English",

volume = "375",

pages = "63--76",

booktitle = "Proceedings of the 11th International Workshop on Theorem Proving Components for Educational Software",

publisher = "EPTCS",

note = "11<sup>th</sup> International Workshop on Theorem Proving Components for Educational Software, Edu ; Conference date: 11-08-2022 Through 12-08-2022",

}

TY - GEN

T1 - On Exams with the Isabelle Proof Assistant

AU - Jacobsen, Frederik Krogsdal

AU - Villadsen, Jørgen

PY - 2023

Y1 - 2023

N2 - 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.

AB - 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.

U2 - 10.4204/EPTCS.375.6

DO - 10.4204/EPTCS.375.6

M3 - Article in proceedings

VL - 375

SP - 63

EP - 76

BT - Proceedings of the 11th International Workshop on Theorem Proving Components for Educational Software

PB - EPTCS

T2 - 11<sup>th</sup> International Workshop on Theorem Proving Components for Educational Software

Y2 - 11 August 2022 through 12 August 2022

ER -

On Exams with the Isabelle Proof Assistant

Abstract

Workshop

Access to Document

OpenUrl availability

Fingerprint

Cite this