NADIA - Natural DeductIon proof Assistant: Um Assistente de provas de Dedução Natural para Lógica Proposicional e Lógica de Predicados
DOI:
https://doi.org/10.5753/rbie.2024.3249Keywords:
Lógica para Computação, Dedução Natural, Assistente de Provas, Ferramenta de Ensino e AprendizagemAbstract
A disciplina de Lógica para Computação faz parte da maioria dos cursos de Tecnologia da Informação e Comunicação. O sistema de Dedução Natural é amplamente utilizado para o ensino de demonstrações e este conteúdo consta em muitos dos livros-texto de Lógica. Este trabalho apresenta um assistente de provas, NADIA Natural Deduction Proof Assistant, para o sistema de Dedução Natural em Lógica Proposicional e Lógica de Predicados, no estilo de Fitch (caixas), com a finalidade de auxiliar no ensino-aprendizagem de estudantes de graduação e pós-graduação. NADIA permite que os estudantes escrevam suas demonstrações de forma mais próxima possível das provas que realizam no papel. NADIA verifica automaticamente se a demonstração está correta e, caso contrário, exibe os erros encontrados. Para avaliar a experiência dos estudantes no uso do NADIA realizamos uma avaliação da ferramenta com alunos de turmas semestrais da disciplina de Lógica para Computação que foram ofertadas nos anos de 2021 e 2022.
Downloads
Referências
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]
Arquivos adicionais
Published
Como Citar
Issue
Section
Licença
Copyright (c) 2024 Davi Romero Vasconcelos, Maria Viviane de Menezes
Este trabalho está licenciado sob uma licença Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.
