Natural Deduction and the Isabelle Proof Assistant
Logic in Computer Science
2018-03-06 v1
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.
Cite
@article{arxiv.1803.01473,
title = {Natural Deduction and the Isabelle Proof Assistant},
author = {Jørgen Villadsen and Andreas Halkjær From and Anders Schlichtkrull},
journal= {arXiv preprint arXiv:1803.01473},
year = {2018}
}
Comments
In Proceedings ThEdu'17, arXiv:1803.00722