NADIA - Natural DeductIon proof Assistant: A Natural Deduction Assistant for Propositional and Predicate Logic
DOI:
https://doi.org/10.5753/rbie.2024.3249Keywords:
Logic in Computer Science, Natural Deduction, Proof Assistant, Teaching ToolsAbstract
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 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 courses that were offered in 2021 and 2022.
Downloads
References
Bornat, R., & Sufrin, B. (1996). Jape’s quiet interface. User Interfaces for Theorem Provers (UITP’96), Technical Report, 25–34. [GS Search]
Chang, C.-L., & Lee, R. C.-T. (1976). Symbolic logic and mechanical theorem proving. Academic press. [GS Search]
da Costa, N. (2008). Introdução aos Fundamentos da Matemática (4a). Hucitec. [GS Search]
da Silva, F., Finger, M., & de Melo, A. (2006). Lógica para Computação. Cengage Learning. [Link] [GS Search]
de Souza, J. (2008). Logica Para Ciencia da Computação. Elsevier. [Link] [GS Search]
Ferreirós, J. (2001). The road to modern logic—an interpretation. Bulletin of Symbolic Logic, 7(4), 441–484. https://doi.org/10.2307/2687794 [GS Search]
Gasquet, O., Schwarzentruber, F., & Strecker, M. (2011). Panda: A Proof Assistant in Natural Deduction for All. A Gentzen Style Proof Assistant for Undergraduate Students. Em P. Blackburn, H. van Ditmarsch, M. Manzano & F. Soler-Toscano (Ed.), Tools for Teaching Logic (pp. 85–92). Springer Berlin Heidelberg. [GS Search]
Gentzen, G. (1969). The collected papers. North-Holland Publishing Company. https://doi.org/10.2307/2272429 [GS Search]
Hammer, E. M. (1998). Semantics for existential graphs. Journal of Philosophical Logic, 27, 489–503. https://doi.org/10.1023/A:1017908108789 [GS Search]
Huth, M., & Ryan, M. (2004). Logic in Computer Science: Modelling and Reasoning about Systems (2nd Ed.). Cambridge University Press. https://doi.org/10.1017/CBO9780511810275 [GS Search]
Leach-Krouse, G. (2018). Carnap: An Open Framework for Formal Reasoning in the Browser. Em P. Quaresma & W. Neuper (Ed.), Proceedings 6th International Workshop on Theorem proving components for Educational software, Gothenburg, Sweden, 6 Aug 2017 (pp. 70–88, Vol. 267). Open Publishing Association. https://doi.org/10.4204/EPTCS.267.5 [GS Search]
Maxim, H., Kaliszyk, C., van Raamsdonk, F., & Wiedijk, F. (2010). Teaching logic using a state-of-art proof assistant. Acta Didactica Napocensia, 3. [Link] [GS Search]
Pelletier, F. J. (1999). A brief history of natural deduction. History and Philosophy of Logic, 20(1), 1–31. https://doi.org/10.1080/014453499298165 [GS Search]
Pelletier, F. J. (2000). A history of natural deduction and elementary logic textbooks. Logical consequence: Rival approaches, 1, 105–138. [GS Search]
Rodríguez-del-Pino, J. C., Rubio Royo, E., & Hernández Figueroa, Z. (2012). A Virtual Programming Lab for Moodle with automatic assessment and anti-plagiarism features. [GS Search]
van Dalen, D. (2013). Logic and Structure (5th Ed.) Springer London. https://doi.org/10.1007/978-1-4471-4558-5 [GS Search]
Vasconcelos, D., Paula, R., & Menezes, M. (2022). NADIA - Natural DeductIon proof Assistant. Anais do XXX Workshop sobre Educação em Computação, 427–438. https://doi.org/10.5753/wei.2022.222875 [GS Search]
Vasconcelos, D. R. (2023). ANITA: Analytic Tableau Proof Assistant. Em P. Quaresma, J. Marcos & W. Neuper (Ed.), Proceedings 11th International Workshop on Theorem Proving Components for Educational Software, Haifa, Israel, 11 August 2022 (pp. 38–53, Vol. 375). Open Publishing Association. https://doi.org/10.4204/EPTCS.375.4 [GS Search]
Villadsen, J., From, A. H., & Schlichtkrull, A. (2018). Natural Deduction and the Isabelle Proof Assistant. Em P. Quaresma & W. Neuper (Ed.), Proceedings 6th International Workshop on Theorem proving components for Educational software, Gothenburg, Sweden, 6 Aug 2017 (pp. 140–155, Vol. 267). Open Publishing Association. https://doi.org/10.4204/EPTCS.267.9 [GS Search]
Additional Files
Published
How to Cite
Issue
Section
License
Copyright (c) 2024 Davi Romero Vasconcelos, Maria Viviane de Menezes
This work is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
