Detecção de Comunidades em Grafos para Adaptação de Granularidade de Demonstrações Matemáticas
Sistemas formais de demonstração matemática têm um 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 (nível de detalhe) que uma demonstração é apresentada. Além de ser fixa, a granularidade das demonstrações apresentadas dentro de sistemas formais não segue uma lógica em relação ao nível de detalhes das asserções utilizadas, por vezes utilizando uma quantidade exagerada de passos elementares em conjunto com passos mais elaborados. O fato de uma demonstração matemática ser construída a partir de teoremas provados previamente permite que essas sejam representadas por grafos conectados acíclicos (árvores). É possível com isso adaptar a granularidade da apresentação de uma demonstração matemática agrupando vértices do grafo de forma a absorver passos que tenham pouca importância do ponto de vista pedagógico. Essa adaptação possibilita que a demonstração seja apresentada de uma forma mais adequada ao nível de conhecimento do estudante, maximizando sua compreensão. Assim, o objetivo dessa pesquisa é utilizar algoritmos de detecção de comunidades em grafos para possibilitar a adaptação da granularidade de uma demonstração matemática construída em um sistema formal a fim de possibilitar ou melhorar seu uso em um contexto de ensino. Como base para a pesquisa será utilizado o sistema formal de demonstração Metamath.