Natural Deduction and the Isabelle Proof Assistant
J{\o}rgen Villadsen (Technical University of Denmark), Andreas, Halkj{\ae}r From (Technical University of Denmark), Anders Schlichtkrull, (Technical University of Denmark)
TL;DR
This paper introduces NaDeA, a natural deduction tool integrated with Isabelle, which offers verified feedback and theorem generation to enhance student learning in formal logic.
Contribution
It presents a novel interface between NaDeA and Isabelle, enabling verified proof feedback and theorem generation for educational purposes.
Findings
NaDeA provides verified feedback to students.
NaDeA generates theorems that can be verified in Isabelle.
The integration enhances learning in formal logic.
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Mathematics, Computing, and Information Processing · Logic, Reasoning, and Knowledge