O Uso de Assistente de Provas no Ensino de Lógica
Resumo
Este resumo tem como objetivo fomentar a discussão sobre a importância do uso de ferramentas computacionais para o ensino de lógica formal em cursos de Bacharelado em Ciência da Computação. Em especial, sugerimos a utilização de assistentes de provas para o desenvolvimento das habilidades presentes em conteúdos introdutórios de lógica e matemática discreta.
Link para o vídeo da apresentação: https://youtu.be/5nwKwVFKW2k
Palavras-chave:
Métodos Formais, Assistente de Provas, Lógica Matemática, Matemática Discreta
Referências
Alison Clear, Tony Clear, Abhijat Vichare, Thea Charles, Stephen Frezza, Mirela Gutica, Barry Lunt, Francesco Maiorana, Arnold Pears, Francois Pitt, Charles Riedesel, and Justyna Szynkiewicz. 2020. Designing Computer Science Competency Statements: A Process and Curriculum Model for the 21st Century. In Proceedings of the Working Group Reports on Innovation and Technology in Computer Science Education (Trondheim, Norway)(ITiCSE-WGR ’20). Association for Computing Machinery, New York, NY, USA, 211–246. https://doi.org/10.1145/3437800.3439208
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen,François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi OuldBiha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and LaurentThéry. 2013. A Machine-Checked Proof of the Odd Order Theorem. In Interactive Theorem Proving 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings (Lecture Notes in Computer Science, Vol. 7998), Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (Eds.). Springer, 163–179. https://doi.org/10.1007/978-3-642-39634-2_14
Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM52,7 (2009), 107–115. https://doi.org/10.1145/1538788.1538814
Georges Gonthier, Andrea Asperti, Jeremy Avigad, Yves Bertot, Cyril Cohen,François Garillot, Stéphane Le Roux, Assia Mahboubi, Russell O’Connor, Sidi OuldBiha, Ioana Pasca, Laurence Rideau, Alexey Solovyev, Enrico Tassi, and LaurentThéry. 2013. A Machine-Checked Proof of the Odd Order Theorem. In Interactive Theorem Proving 4th International Conference, ITP 2013, Rennes, France, July 22-26, 2013. Proceedings (Lecture Notes in Computer Science, Vol. 7998), Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (Eds.). Springer, 163–179. https://doi.org/10.1007/978-3-642-39634-2_14
Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM52,7 (2009), 107–115. https://doi.org/10.1145/1538788.1538814
Publicado
26/04/2021
Como Citar
RIBEIRO, Rodrigo Geraldo; ROGGIA, Karina; VASCONCELLOS, Cristiano.
O Uso de Assistente de Provas no Ensino de Lógica. In: LABORATÓRIO DE IDEIAS - SIMPÓSIO BRASILEIRO DE EDUCAÇÃO EM COMPUTAÇÃO (EDUCOMP), 1. , 2021, On-line.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2021
.
p. 05-05.
DOI: https://doi.org/10.5753/educomp_estendido.2021.14846.
