NADIA - Natural DeductIon proof Assistant
Abstract
Logic in Computer Science course is part of most Information and Communication Technology courses. The Natural Deduction system is widely used for teaching proofs and appears in many Logic textbooks. This work presents a proof assistant, NADIA (Natural Deduction Proof Assistant), for Natural Deduction system, in the Fitch (boxes) style, in order to assist in the teaching-learning of undergraduate and graduate students. NADIA allows students to write their proofs as closely as possible to the proofs they take on paper. NADIA automatically checks whether the proof is correct and, if not, displays any errors found. To assess students' experience in using NADIA, we performed an evaluation of the tool in five courses that were offered in 2021.1 and 2021.2.
References
Chang, C.-L. and Lee, R. C.-T. (1976). Symbolic logic and mechanical theorem proving. Academic press.
da Costa, N. (2008). Introdução aos Fundamentos da Matemática. Hucitec, 4a edition.
Gasquet, O., Schwarzentruber, F., and Strecker, M. (2011). Panda: A proof assistant in natural deduction for all. a gentzen style proof assistant for undergraduate students. In Blackburn, P., van Ditmarsch, H., Manzano, M., and Soler-Toscano, F., editors, Tools for Teaching Logic, pages 85–92, Berlin, Heidelberg. Springer Berlin Heidelberg.
Gentzen, G. (1969). The collected papers. North-Holland Publishing Company.
Huth, M. and Ryan, M. D. (2004). Logic in computer science - modelling and reasoning about systems (2. ed.). Cambridge University Press.
Maxim, H., Kaliszyk, C., van Raamsdonk, F., and Wiedijk, F. (2010). Teaching logic using a state-of-art proof assistant. Acta Didactica Napocensia, 3.
Pelletier, F. J. (1999). A brief history of natural deduction. History and Philosophy of Logic, 20(1):1–31.
Pelletier, F. J. (2000). A history of natural deduction and elementary logic textbooks. Logical consequence: Rival approaches, 1:105–138.
van Dalen, D. (1994). Logic and structure (3. ed.). Universitext. Springer.
