15 citations · 93 across the 15 of their papers we have counts for
17 papers
ProofBuddy: A Proof Assistant for Learning and Monitoring
Nadine Karsten, Frederik Krogsdal Jacobsen, Kim Jana Eiken +2
Proof competence, i.e. the ability to write and check (mathematical) proofs, is an important skill in Computer Science, but for many students it represents a difficult challenge. T…
On Exams with the Isabelle Proof Assistant
Frederik Krogsdal Jacobsen, Jørgen Villadsen
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 unde…
Teaching Functional Programmers Logic and Metatheory
Frederik Krogsdal Jacobsen, Jørgen Villadsen
We present a novel approach for teaching logic and the metatheory of logic to students who have some experience with functional programming. We define concepts in logic as a series…
SeCaV: A Sequent Calculus Verifier in Isabelle/HOL
Asta Halkjær From, Frederik Krogsdal Jacobsen, Jørgen Villadsen
We describe SeCaV, a sequent calculus verifier for first-order logic in Isabelle/HOL, and the SeCaV Unshortener, an online tool that expands succinct derivations into the full SeCa…
Teaching Intuitionistic and Classical Propositional Logic Using Isabelle
Jørgen Villadsen, Asta Halkjær From, Patrick Blackburn
We describe a natural deduction formalization of intuitionistic and classical propositional logic in the Isabelle/Pure framework. In contrast to earlier work, where we explored the…
Isabelle/HOL as a Meta-Language for Teaching Logic
Asta Halkjær From, Jørgen Villadsen, Patrick Blackburn
Proof assistants are important tools for teaching logic. We support this claim by discussing three formalizations in Isabelle/HOL used in a recent course on automated reasoning. Th…