15 citations · 93 across the 15 of their papers we have counts for
11 papers · 1 filter
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…
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…
Teaching a Formalized Logical Calculus
Asta Halkjær From, Alexander Birch Jensen, Anders Schlichtkrull +1
Classical first-order logic is in many ways central to work in mathematics, linguistics, computer science and artificial intelligence, so it is worthwhile to define it in full deta…