# Natural Deduction and the Isabelle Proof Assistant

arXiv: https://arxiv.org/abs/1803.01473 · HTML: https://mlsanity.com/paper/1803.01473/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 5 Mar 2018.

## Built on by (most cited first, 1 of 1)

- [Teaching Higher-Order Logic Using Isabelle](https://mlsanity.com/paper/2404.05458/) (2024)

## Abstract (arXiv)

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.