NaDeA: A Natural Deduction Assistant with a Formalization in Isabelle

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

242 Downloads (Pure)

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.
Original languageEnglish
Title of host publicationProceedings of the Fourth International Conference on Tools for Teaching Logic (TTL 2015)
Publication date2015
Pages253-262
Publication statusPublished - 2015
Event4th International Conference on Tools for Teaching Logic (TTL 2015) - Rennes, France
Duration: 9 Jun 201512 Jun 2015
Conference number: 4
http://ttl2015.irisa.fr/

Conference

Conference4th International Conference on Tools for Teaching Logic (TTL 2015)
Number4
CountryFrance
CityRennes
Period09/06/201512/06/2015
Internet address

Keywords

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

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

Cite this