Natural Deduction and the Isabelle Proof Assistant
Not on the map. Why?
Abstract (arXiv)
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 that has been verified in Isabelle, provides feedback to the student, and also how NaDeA, for each formula proved by the student, provides a generated theorem that can be verified in Isabelle.
Key facts. Cited by 1 paper in the map (data through 14 Oct 2026). First posted on arXiv 5 Mar 2018.
Builds on
No reference list yet.
Built on by
Citing papers per year: 2024: 1.
1 paper.
- 2024Teaching Higher-Order Logic Using Isabellecited by 0
- 2024Teaching Higher-Order Logic Using Isabelle8 Apr 2024