Banca de DEFESA: LUCAS VIEIRA DE OLIVEIRA

Uma banca de DEFESA de MESTRADO foi cadastrada pelo programa.
STUDENT : LUCAS VIEIRA DE OLIVEIRA
DATE: 28/11/2022
TIME: 14:00
LOCAL: https://conferenciaweb.rnp.br/webconf/edson-2
TITLE:

Comparison of Criteria for Adaptation of Granularity of Mathematical Proofs using the Metamath Environment

PAGES: 110
BIG AREA: Ciências Exatas e da Terra
AREA: Ciência da Computação
SUMMARY:

Formal mathematical proof systems are crucial in improving and developing new proofs. Furthermore, the methods and structures involved in formal systems have the potential to support the development of tutoring systems for learning demonstrations, which several works have already done. However, the fact that these formal systems do not have pedagogical objectives as their main motivation brings some obstacles to their use in a teaching context. One such issue is granularity, that is, the level of detail at which a demo is presented. Evidence presented within formal systems requires that all steps be deduced explicitly, making its interpretation difficult since even inferences considered obvious for specific audiences must be presented, which sometimes makes the proof excessively long. Adapting the presentation of a formal proof so that obvious inferences are omitted, as in the presentation of mathematical proofs in natural language, is not a trivial task since in principle, there are no clear standards that can be used for this purpose. Some works have studied this problem in the last decades. However, several of them use different representations and data. This fragmentation makes it difficult for advances in the area to be researched, as it prevents the direct comparison of the different methods used and their comparison with possible new methods. Thus, this research aims to compare different methods of adapting the granularity of mathematical proofs around the same representation and data set to identify which patterns are more effective. In addition to comparing methods already proposed in other works, a proof of concept is also made using machine learning as a contribution to the advancement of the area.

BANKING MEMBERS:
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