Formal Methods Online: Natural Deduction Assistant (NaDeA)

Research output: Contribution to conferenceConference abstract for conferenceResearchpeer-review

9 Downloads (Pure)


We present the Natural Deduction Assistant (NaDeA) and discuss its advantages and disadvantages as a tool for teaching logic, automated reasoning and formal methods. NaDeA is a browser application for classical first-order logic with constants and functions. The syntax, the semantics and the inductive definition of the natural deduction proof system along with the soundness and completeness proofs are verified in Isabelle/HOL. Finished NaDeA proofs are automatically translated into the corresponding Isabelle-embedded proofs. Hundreds of computer science students have used NaDeA for course exercises and exams since 2015.
Original languageEnglish
Publication date2021
Number of pages1
Publication statusPublished - 2021
EventFormal Methods Education Online - Virtual Event
Duration: 12 Jul 202112 Jul 2021


ConferenceFormal Methods Education Online
LocationVirtual Event


Dive into the research topics of 'Formal Methods Online: Natural Deduction Assistant (NaDeA)'. Together they form a unique fingerprint.

Cite this