Natural Deduction and the Isabelle Proof Assistant

Jørgen Villadsen*, Andreas Halkjær From, Anders Schlichtkrull

*Corresponding author for this work

Research output: Contribution to journalJournal articleResearchpeer-review

271 Downloads (Pure)

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 languageEnglish
JournalElectronic Proceedings in Theoretical Computer Science
Volume267
Pages (from-to)140-155
ISSN2075-2180
DOIs
Publication statusPublished - 2018
Event6th International Workshop
on Theorem proving components for Educational software
- Gothenburg, Sweden
Duration: 6 Aug 20176 Aug 2017

Conference

Conference6th International Workshop
on Theorem proving components for Educational software
CountrySweden
CityGothenburg
Period06/08/201706/08/2017

Fingerprint

Dive into the research topics of 'Natural Deduction and the Isabelle Proof Assistant'. Together they form a unique fingerprint.

Cite this