Navegando por Autor "Lopes Neto, João Mendes"
Agora exibindo 1 - 1 de 1
- Resultados por página
- Opções de Ordenação
Dissertação Um método para geração automatizada de exercícios de demonstração com um nível de complexidade similar(Universidade Federal do Rio Grande do Norte, 2025-07-21) Lopes Neto, João Mendes; Almeida, João Marcos de; Terrematte, Patrick César Alves; https://orcid.org/0000-0002-0385-0030; http://lattes.cnpq.br/4283045850342312; https://orcid.org/0000-0003-2601-8164; http://lattes.cnpq.br/3059324458238110; http://lattes.cnpq.br/2653822875045890; Santiago, Regivan Hugo Nunes; http://lattes.cnpq.br/7536988783793885; Olarte, Carlos; http://lattes.cnpq.br/1198550954813139; Seca Neto, Adolfo Gustavo Serra; https://orcid.org/0000-0002-0260-5922; http://lattes.cnpq.br/0071119715272492; Nalon, Cláudia; https://orcid.org/0000-0002-9792-5346; http://lattes.cnpq.br/7793795625581127A geração automatizada de exercícios pode beneficiar educadores ao reduzir significativamente o tempo que gastam na elaboração manual de exercícios. No entanto, um obstáculo para tornar essa automação mais presente na rotina profissional de um educador é o controle do nível de complexidade de exercícios gerados mecanicamente. Neste trabalho, apresentamos um método para a geração automatizada de exercícios de demonstração com um nível de complexidade similar. As entradas deste método são um exercício de demonstração e um conjunto de regras as quais permitem demonstrar este exercício. A saída é um conjunto de exercícios de demonstração com uma complexidade similar à do exercício passado como entrada. O escopo dos exercícios com os quais trabalhamos são exercícios de demonstração matemática descritos em linguagens de primeira ordem, cobrindo tópicos como Teoria dos Conjuntos e Teoria dos Números. Para calcular o nível de complexidade destes exercícios, fundamentamos a nossa abordagem no esforço necessário para os resolver através de demonstrações informais. Argumentamos que esse esforço, por sua vez, pode ser capturado por demonstrações formais em tablôs baseados em corte que não contêm símbolos lógicos. As regras utilizadas nestas demonstrações são extraídas por um procedimento mecanizável que fornecemos. Usamos o carácter analítico dessas regras e a estrutura formal que as demonstrações de tablô têm para fornecer um procedimento computacional do método em questão. Como casos de estudo, demonstramos como o nosso método funciona com fragmentos da Teoria dos Conjuntos e da Teoria dos Números. Uma implementação prototípica também foi desenvolvida e nós a apresentamos aqui.