15 citations · 32 across the 4 of their papers we have counts for
4 papers · 1 filter
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…
Natural Deduction and the Isabelle Proof Assistant
Jørgen Villadsen, Andreas Halkjær From, Anders Schlichtkrull
We describe our Natural Deduction Assistant (NaDeA) and the interfaces between the Isabelle proof assistant and NaDeA. In particular, we explain how NaDeA, using a generated prover…