Comparação de Critérios para Adaptação de Granularidade de Provas Matemáticas utilizando a Ambiente Metamath
Sistemas formais de demonstração matemática têm papel fundamental no aprimoramento e desenvolvimento de novas demonstrações. Além disso, os métodos e estruturas envolvidos em sistemas formais têm o potencial de apoiar o desenvolvimento de sistemas de tutoria para o aprendizado de demonstrações, o que já tem sido feito por diversos trabalhos. No entanto, o fato destes sistemas formais não terem objetivos pedagógicos como motivação principal, traz alguns obstáculos para o seu uso em um contexto de ensino. Um desses problemas é a granularidade, ou seja, o nível de detalhes em que uma demonstração é apresentada. Provas apresentadas dentro de sistemas formais necessitam que todos os passos sejam deduzidos explicitamente, dificultando sua interpretação, já que mesmo inferências consideradas óbvias para determinadas audiências devem ser exibidas, o que em alguns casos deixa a prova excessivamente longa. Adaptar a apresentação de uma prova formal para que inferências óbvias sejam omitidas, como na apresentação de provas matemáticas em linguagem natural, não é uma tarefa trivial, já que a princípio não existem padrões claros que possam ser utilizados para este fim. Alguns trabalhos têm estudado esse problema nas últimas décadas, no entanto, vários deles utilizando representações e dados diferentes. Essa fragmentação dificulta que avanços na área sejam pesquisados, já que impede a comparação direta dos diferentes métodos utilizados e sua comparação com possíveis novos métodos. Assim, o objetivo dessa pesquisa é comparar diferentes métodos de adaptação de granularidade de provas matemáticas em torno de uma mesma representação e mesmo conjunto de dados, a fim de identificar quais padrões são mais efetivos. Além da comparação de métodos já propostos em outros trabalhos, também é feita uma prova de conceito utilizando aprendizagem de máquina como contribuição para o avanço da área.