Conference paper
Formal Methods Online: Natural Deduction Assistant (NaDeA)
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.
Language: | English |
---|---|
Year: | 2021 |
Proceedings: | Formal Methods Education Online |
Types: | Conference paper |
ORCIDs: | Villadsen, Jørgen |