Natural Deduction and the Isabelle Proof Assistant
arXiv:1803.01473 · doi:10.4204/EPTCS.267.9
Abstract
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.
arXiv commentIn Proceedings ThEdu'17, arXiv:1803.00722
Cited by in corpus (8)
- Natural Deduction Assistant (NaDeA)
- Isabelle/HOL as a Meta-Language for Teaching Logic
- ANITA: Analytic Tableau Proof Assistant
- Students' Proof Assistant (SPA)
- Teaching Intuitionistic and Classical Propositional Logic Using Isabelle
- ProofBuddy: A Proof Assistant for Learning and Monitoring
- Proof Assistants for Teaching: a Survey
- Teaching Higher-Order Logic Using Isabelle