Electronic Proceedings in Theoretical Computer Science (Mar 2018)

Natural Deduction and the Isabelle Proof Assistant

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

DOI
https://doi.org/10.4204/EPTCS.267.9
Journal volume & issue
Vol. 267, no. Proc. ThEdu 2017
pp. 140 – 155

Abstract

Read online

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.