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

Asta Halkjær From, Helge Hatteland, Jørgen Villadsen

Research output: Contribution to conferencePaperResearchpeer-review

93 Downloads (Pure)


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
Event10th Scandinavian Logic Symposium - University of Gothenburg, Gothenburg, Sweden
Duration: 11 Jun 201813 Jun 2018
Conference number: 10


Conference10th Scandinavian Logic Symposium
LocationUniversity of Gothenburg
Internet address

Bibliographical note



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

Cite this