Aplicação do Provador de Teoremas LEAN no Ensino de Lógica Matemática para Alunos de Sistemas de Informação: Um Estudo de Caso
Resumo
Este trabalho investiga o uso do provador de teoremas LEAN no ensino de lógica matemática para estudantes de Sistemas de Informação. Embora a avaliação quantitativa do impacto do LEAN no aprendizado dos alunos tenha sido adiada devido a uma greve, este estudo documenta detalhadamente a implementação de problemas de lógica proposicional usando o LEAN. O foco está na aplicação do LEAN para resolver problemas selecionados e na análise de como a ferramenta pode ser usada para explorar conceitos lógicos. Essa abordagem serve como base para futuras avaliações empíricas sobre a eficácia dessa metodologia no ensino de lógica matemática.
Palavras-chave:
Lógica Matemática, Provador de Teoremas LEAN, Ensino de Sistemas de Informação, Ferramentas Computacionais, Metodologia Educacional
Referências
Avigad, J., De Moura, L., and Kong, S. (2015). Theorem proving in lean. Release, 3(0):1–4.
Avigad, J., Hölzl, J., and Serafin, L. (2017). A formally verified proof of the central limit theorem. Journal of Automated Reasoning, 59(4):389–423.
Avigad, J., Lewis, R. Y., and van Doorn, F. (2020). Logic and Proof. Lecture notes for the course Logic and Mathematical Inquiry.
Avigad, J. and Massot, P. (2024). Mathematics in lean. Technical Report Release 0.1, Lean Community.
Charles Fadel, Maya Bialik, e. B. T. (2015). Four-Dimensional Education: The Competencies Learners Need to Succeed. Solution Tree Press.
Cherniavsky, J. and Heeren, C. (2017). Self-Adaptive Systems for Machine Intelligence. IGI Global.
De Moura, L., Kong, S., Avigad, J., Van Doorn, F., and von Raumer, J. (2015). The LEAN theorem prover (system description). In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pages 378–388. Springer.
Feofiloff, P. and Szwarcfiter, J. L. (2009). Algoritmos e Estruturas de Dados. LTC.
Gersting, J. L. (2019). Fundamentos Matemáticos Para a Ciência Da Computação: Matemática Discreta e Suas Aplicações. LTC, Rio de Janeiro, RJ, 7ª edição edition.
Huth, M. and Ryan, M. (2007). Lógica Em Ciência Da Computação: Modelagem e Argumentação Sobre Sistemas. LTC - Livros Tecnicos E Cientificos Editora Lda.
Plainer, M. (2021). Practical study of visual studio code. techreport, Technical University of Munich.
Avigad, J., Hölzl, J., and Serafin, L. (2017). A formally verified proof of the central limit theorem. Journal of Automated Reasoning, 59(4):389–423.
Avigad, J., Lewis, R. Y., and van Doorn, F. (2020). Logic and Proof. Lecture notes for the course Logic and Mathematical Inquiry.
Avigad, J. and Massot, P. (2024). Mathematics in lean. Technical Report Release 0.1, Lean Community.
Charles Fadel, Maya Bialik, e. B. T. (2015). Four-Dimensional Education: The Competencies Learners Need to Succeed. Solution Tree Press.
Cherniavsky, J. and Heeren, C. (2017). Self-Adaptive Systems for Machine Intelligence. IGI Global.
De Moura, L., Kong, S., Avigad, J., Van Doorn, F., and von Raumer, J. (2015). The LEAN theorem prover (system description). In Automated Deduction-CADE-25: 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings 25, pages 378–388. Springer.
Feofiloff, P. and Szwarcfiter, J. L. (2009). Algoritmos e Estruturas de Dados. LTC.
Gersting, J. L. (2019). Fundamentos Matemáticos Para a Ciência Da Computação: Matemática Discreta e Suas Aplicações. LTC, Rio de Janeiro, RJ, 7ª edição edition.
Huth, M. and Ryan, M. (2007). Lógica Em Ciência Da Computação: Modelagem e Argumentação Sobre Sistemas. LTC - Livros Tecnicos E Cientificos Editora Lda.
Plainer, M. (2021). Practical study of visual studio code. techreport, Technical University of Munich.
Publicado
17/10/2024
Como Citar
VANELI, Willian B.; ANDRADE, Jefferson O..
Aplicação do Provador de Teoremas LEAN no Ensino de Lógica Matemática para Alunos de Sistemas de Informação: Um Estudo de Caso. In: ESCOLA REGIONAL DE INFORMÁTICA DO ESPÍRITO SANTO, 9. , 2024, Vitória/ES.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2024
.
p. 99-106.
DOI: https://doi.org/10.5753/eries.2024.244646.
