Natural Deduction and the Isabelle Proof Assistant

Publication: Research - peer-reviewJournal article – Annual report year: 2018

Documents

DOI

View graph of relations

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
StatePublished - 2018
Event6th International Workshop
on Theorem proving components for Educational software - Gothenburg, Sweden

Conference

Conference6th International Workshop
on Theorem proving components for Educational software
CountrySweden
CityGothenburg
Period06/08/201706/08/2017
CitationsWeb of Science® Times Cited: No match on DOI
Download as:
Download as PDF
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
PDF
Download as HTML
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
HTML
Download as Word
Select render style:
APAAuthorCBE/CSEHarvardMLAStandardVancouverShortLong
Word

Download statistics

No data available

ID: 144428404