Natural Deduction and the Isabelle Proof Assistant

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.

In Pedro Quaresma and Walther Neuper: Proceedings 6th International Workshop on Theorem proving components for Educational software (ThEdu'17), Gothenburg, Sweden, 6 Aug 2017, Electronic Proceedings in Theoretical Computer Science 267, pp. 140–155.
Published: 2nd March 2018.

ArXived at: http://dx.doi.org/10.4204/EPTCS.267.9 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org