NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle
Abstract
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 undergraduate computer science 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.
Keywords
Cite
@article{arxiv.1507.04002,
title = {NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle},
author = {Jørgen Villadsen and Alexander Birch Jensen and Anders Schlichtkrull},
journal= {arXiv preprint arXiv:1507.04002},
year = {2015}
}
Comments
Proceedings of the Fourth International Conference on Tools for Teaching Logic (TTL2015), Rennes, France, June 9-12, 2015. Editors: M. Antonia Huertas, Jo\~ao Marcos, Mar\'ia Manzano, Sophie Pinchinat, Fran\c{c}ois Schwarzentruber