NADIA - Natural DeductIon proof Assistant: Un Asistente de Pruebas de Deducción Natural para Lógica Proposicional y Lógica de Predicados
DOI:
https://doi.org/10.5753/rbie.2024.3249Keywords:
Lógica para Computación, Deducción Natural, Asistente de Pruebas, Herramienta de Enseñanza y AprendizajeAbstract
La disciplina de Lógica para Computación forma parte de la mayoría de los cursos de Tecnología de la Información y Comunicación. El sistema de Deducción Natural es ampliamente utilizado para la enseñanza de demostraciones y este contenido aparece en muchos de los libros de texto de Lógica. Este trabajo presenta un asistente de pruebas, NADIA (Natural Deduction Proof Assistant), para el sistema de Deducción Natural en Lógica Proposicional y Lógica de Predicados, en el estilo de Fitch (con cajas), con el propósito de ayudar en la enseñanza-aprendizaje de estudiantes de grado y posgrado. NADIA permite que los estudiantes escriban sus demostraciones de la manera más cercana posible a las pruebas que realizan en papel. NADIA verifica automáticamente si la demostración es correcta y, en caso contrario, muestra los errores encontrados. Para evaluar la experiencia de los estudiantes en el uso de NADIA, realizamos una evaluación de la herramienta con alumnos de clases semestrales de la disciplina de Lógica para Computación ofrecidas en los años 2021 y 2022.
Descargas
Citas
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]
Archivos adicionales
Published
Cómo citar
Issue
Section
Licencia
Derechos de autor 2024 Davi Romero Vasconcelos, Maria Viviane de Menezes
Esta obra está bajo una licencia internacional Creative Commons Atribución-NoComercial-SinDerivadas 4.0.
