Abstract
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 language | English |
|---|---|
| Publication date | 2021 |
| Number of pages | 1 |
| Publication status | Published - 2021 |
| Event | Formal Methods Education Online - Virtual Event Duration: 12 Jul 2021 → 12 Jul 2021 |
Conference
| Conference | Formal Methods Education Online |
|---|---|
| Location | Virtual Event |
| Period | 12/07/2021 → 12/07/2021 |