Natural Deduction Assistant (NaDeA)

Natural Deduction Assistant (NaDeA)

We present the Natural Deduction Assistant (NaDeA) and discuss its advantages and disadvantages as a tool for teaching logic. NaDeA is available online and is based on a formalization of natural deduction in the Isabelle proof assistant. We first provide concise formulations of the main formalizatio...

Full description

Bibliographic Details
Main Authors: Jørgen Villadsen, Andreas Halkjær From, Anders Schlichtkrull
Format: Article
Language:English
Published: Open Publishing Association 2019-04-01
Series:Electronic Proceedings in Theoretical Computer Science
Online Access:http://arxiv.org/pdf/1904.00618v1
id doaj-d24aea4e8d8245e783d6d6548ea14902
record_format Article
spelling doaj-d24aea4e8d8245e783d6d6548ea149022020-11-25T02:18:59ZengOpen Publishing AssociationElectronic Proceedings in Theoretical Computer Science2075-21802019-04-01290Proc. ThEdu 2018142910.4204/EPTCS.290.2:17Natural Deduction Assistant (NaDeA)Jørgen Villadsen0Andreas Halkjær From1Anders Schlichtkrull2 Technical University of Denmark Technical University of Denmark Technical University of Denmark We present the Natural Deduction Assistant (NaDeA) and discuss its advantages and disadvantages as a tool for teaching logic. NaDeA is available online and is based on a formalization of natural deduction in the Isabelle proof assistant. We first provide concise formulations of the main formalization results. We then elaborate on the prerequisites for NaDeA, in particular we describe a formalization in Isabelle of "Hilbert's Axioms" that we use as a starting point in our bachelor course on mathematical logic. We discuss a recent evaluation of NaDeA and also give an overview of the exercises in NaDeA.http://arxiv.org/pdf/1904.00618v1
collection DOAJ
language English
format Article
sources DOAJ
author Jørgen Villadsen
Andreas Halkjær From
Anders Schlichtkrull
spellingShingle Jørgen Villadsen
Andreas Halkjær From
Anders Schlichtkrull
Natural Deduction Assistant (NaDeA)
Electronic Proceedings in Theoretical Computer Science
author_facet Jørgen Villadsen
Andreas Halkjær From
Anders Schlichtkrull
author_sort Jørgen Villadsen
title Natural Deduction Assistant (NaDeA)
title_short Natural Deduction Assistant (NaDeA)
title_full Natural Deduction Assistant (NaDeA)
title_fullStr Natural Deduction Assistant (NaDeA)
title_full_unstemmed Natural Deduction Assistant (NaDeA)
title_sort natural deduction assistant (nadea)
publisher Open Publishing Association
series Electronic Proceedings in Theoretical Computer Science
issn 2075-2180
publishDate 2019-04-01
description We present the Natural Deduction Assistant (NaDeA) and discuss its advantages and disadvantages as a tool for teaching logic. NaDeA is available online and is based on a formalization of natural deduction in the Isabelle proof assistant. We first provide concise formulations of the main formalization results. We then elaborate on the prerequisites for NaDeA, in particular we describe a formalization in Isabelle of "Hilbert's Axioms" that we use as a starting point in our bachelor course on mathematical logic. We discuss a recent evaluation of NaDeA and also give an overview of the exercises in NaDeA.
url http://arxiv.org/pdf/1904.00618v1
work_keys_str_mv AT jørgenvilladsen naturaldeductionassistantnadea
AT andreashalkjærfrom naturaldeductionassistantnadea
AT andersschlichtkrull naturaldeductionassistantnadea
_version_ 1724879455051055104

Similar Items