Jørgen Villadsen (Technical University of Denmark) |
Andreas Halkjær From (Technical University of Denmark) |
Anders Schlichtkrull (Technical University of Denmark) |
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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.267.9 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |