NADIA - Natural DeductIon proof Assistant
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.
Referências
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.
