PPGCCM PÓS-GRADUAÇÃO EM CIÊNCIA DA COMPUTAÇÃO FUNDAÇÃO UNIVERSIDADE FEDERAL DO ABC Telefone/Ramal: 11 4996-8337 http://propg.ufabc.edu.br/ppgccm

Banca de DEFESA: LUCAS VIEIRA DE OLIVEIRA

Uma banca de DEFESA de MESTRADO foi cadastrada pelo programa.
DISCENTE : LUCAS VIEIRA DE OLIVEIRA
DATA : 28/11/2022
HORA: 14:00
LOCAL: https://conferenciaweb.rnp.br/webconf/edson-2
TÍTULO:

Comparação de Critérios para Adaptação de Granularidade de Provas Matemáticas utilizando a Ambiente Metamath



PÁGINAS: 110
RESUMO:

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.



MEMBROS DA BANCA:
Presidente - Interno ao Programa - 1672965 - EDSON PINHEIRO PIMENTEL
Membro Titular - Examinador(a) Interno ao Programa - 1934625 - JESUS PASCUAL MENA CHALCO
Membro Titular - Examinador(a) Externo à Instituição - PATRICIA AUGUSTIN JAQUES MAILARD - UFPR
Membro Suplente - Examinador(a) Interno ao Programa - 1672977 - JOAO PAULO GOIS
Membro Suplente - Examinador(a) Externo à Instituição - ISMAR FRANGO SILVEIRA - UNICRUZ
Notícia cadastrada em: 31/10/2022 17:07
SIGAA | UFABC - Núcleo de Tecnologia da Informação - ||||| | Copyright © 2006-2024 - UFRN - sigaa-1.ufabc.int.br.sigaa-1-prod