15 citations · 59 across the 6 of their papers we have counts for
7 papers
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…
Natural Deduction Assistant (NaDeA)
Jørgen Villadsen, Andreas Halkjær From, Anders Schlichtkrull
We present the Natural Deduction Assistant (NaDeA) and discuss its advantages and disadvantages as a tool for teaching logic. NaDeA is available online and is based on a formalizat…
Students' Proof Assistant (SPA)
Anders Schlichtkrull, Jørgen Villadsen, Andreas Halkjær From
The Students' Proof Assistant (SPA) aims to both teach how to use a proof assistant like Isabelle and also to teach how reliable proof assistants are built. Technically it is a min…