Teaching First-Order Logic with the Natural Deduction Assistant (NaDeA)

Research output: Contribution to conferencePaperResearchpeer-review

82 Downloads (Pure)

Abstract

The natural deduction proof system is a popular way of teaching logic. It is also important in the philosophy of logic and the foundations of mathematics, in particular for systems of intuitionistic logic and constructive type theory, and it is used in many proof assistants along with automatic proof methods like the tableaux procedure and the resolution calculus. The natural deduction assistant (NaDeA) has been used for teaching first-order logic to hundreds of computer science bachelor students since 2015 [1, 2]. NaDeA runs in a standard browser and is open source software. Upon completion of a natural deduction proof the student obtains a formal proof in the interactive proof assistant Isabelle/HOL [3] of not only the correctness of the student’s natural deduction proof but also of the validity of the formula with respect to the classical semantics of formulas in first-order logic. Our formalization of the syntax, semantics and the inductive definition of the natural deduction proof system extends work by Stefan Berghofer [4] and Melvin Fitting [5] but with a much more detailed soundness proof that can be examined and tested by the students. The corresponding completeness proof is also available but it is of course quite demanding. We describe the main advantages and disadvantages of using an advanced e-learning tools like NaDeA for teaching logic. Furthermore we briefly survey related and future work. NaDeA can be used with or without installing Isabelle and is available online. URL Address: https://nadea.compute.dtu.dk/.
Original languageEnglish
Publication date2018
Number of pages1
Publication statusPublished - 2018
EventTenth Scandinavian Logic Symposium - University of Gothenburg, Gothenburg, Sweden
Duration: 11 Jun 201813 Jun 2018
http://scandinavianlogic.org/sls2018

Conference

ConferenceTenth Scandinavian Logic Symposium
LocationUniversity of Gothenburg
Country/TerritorySweden
CityGothenburg
Period11/06/201813/06/2018
Internet address

Bibliographical note

http://scandinavianlogic.org/material/book_of_abstracts_sls2018.pdf

Fingerprint

Dive into the research topics of 'Teaching First-Order Logic with the Natural Deduction Assistant (NaDeA)'. Together they form a unique fingerprint.

Cite this