NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle

Research output: Contribution to journalJournal articleResearchpeer-review

340 Downloads (Pure)


We present a new software tool for teaching logic based on natural deduction. Its proof system is formalized in the proof assistant Isabelle such that its definition is very precise. Soundness of the formalization has been proved in Isabelle. The tool is open source software developed in TypeScript / JavaScript and can thus be used directly in a browser without any further installation. Although developed for computer science bachelor students who are used to study and program concrete computer code in a programming language we consider the approach relevant for a broader audience and for other proof systems as well.
Original languageEnglish
JournalIfCoLog Journal of Logics and their Applications
Issue number1
Pages (from-to)55-82
Publication statusPublished - 2017

Bibliographical note

This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.


  • Natural Deduction
  • Formalization
  • Isabelle Proof Assistant
  • First-Order Logic
  • Higher-Order Logic


Dive into the research topics of 'NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle'. Together they form a unique fingerprint.

Cite this