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.
| Original language | English |
|---|---|
| Journal | Electronic Proceedings in Theoretical Computer Science |
| Volume | 267 |
| Pages (from-to) | 140-155 |
| ISSN | 2075-2180 |
| DOIs | |
| Publication status | Published - 2018 |
| Event | 6th International Workshop on Theorem proving components for Educational Software - Gothenburg, Sweden Duration: 6 Aug 2017 → 6 Aug 2017 Conference number: 6 |
Workshop
| Workshop | 6th International Workshop on Theorem proving components for Educational Software |
|---|---|
| Number | 6 |
| Country/Territory | Sweden |
| City | Gothenburg |
| Period | 06/08/2017 → 06/08/2017 |