NADIA - Natural DeductIon proof Assistant

  • Davi Romero de Vasconcelos UFC
  • Robson Teixeira Paula UFC
  • Maria Viviane Menezes UFC

Resumo


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, 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 cinco turmas da disciplina de Lógica para Computação que foram ofertadas em 2021.1 e 2021.2.

Palavras-chave: Lógica para Computação, Assistente de Provas, Dedução Natural

Referências

Bornat, R. and Sufrin, B. (1996). Jape’s quiet interface.

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.
Publicado
31/07/2022
VASCONCELOS, Davi Romero de; PAULA, Robson Teixeira; MENEZES, Maria Viviane. NADIA - Natural DeductIon proof Assistant. In: WORKSHOP SOBRE EDUCAÇÃO EM COMPUTAÇÃO (WEI), 30. , 2022, Niterói. Anais [...]. Porto Alegre: Sociedade Brasileira de Computação, 2022 . p. 427-438. ISSN 2595-6175. DOI: https://doi.org/10.5753/wei.2022.222875.