On Exams with the Isabelle Proof Assistant

要約

イザベル証明アシスタントを使用して、自動推論のコースで学生の学習成果をテストするためのアプローチを提示します。
このアプローチにより、さまざまな論理的証明システムにおける形式的証明の一般的な理解と、特に Isabelle/HOL の高階論理における証明の理解の両方をテストできます。
Isabelle を使用すると、試験の大部分をほぼ自動的に採点できます。
いくつかの問題例を通して私たちのアプローチを説明し、選択した種類の問題のそれぞれが意図した学習成果の適切な尺度であると私たちが信じる理由を説明します.
最後に、自動推論に関するコースの試験のアプローチを使用した経験について説明し、将来の作業の可能性を提案します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google