Banca de DEFESA: JOÃO MENDES LOPES NETO

Uma banca de DEFESA de MESTRADO foi cadastrada pelo programa.
STUDENT : JOÃO MENDES LOPES NETO
DATE: 21/07/2025
TIME: 09:00
LOCAL: Google Meet
TITLE:

A method for automated generation of proof exercises with comparable level of complexity

KEY WORDS:

Automatic Question Generation, Teaching Logic, Cut-based tableaux

PAGES: 112
BIG AREA: Ciências Exatas e da Terra
AREA: Ciência da Computação
SUBÁREA: Teoria da Computação
SPECIALTY: Lógicas e Semântica de Programas
SUMMARY:

The automated generation of exercises may benefit educators by significantly reducing the time they spend in manually creating exercises. However, an obstacle in making such automation more present in an educator's professional routine is controlling the level of complexity of mechanically generated exercises. In this work, we present a method for the automated generation of proof exercises with comparable level of complexity. The inputs of this method are a proof exercise and a set of rules allowing to prove this exercise. The output is a set of proof exercises with comparable complexity to that of given as input. The scope of exercises we work with are mathematical proof exercises described in first-order languages, covering topics such as Set Theory and Number Theory. In order to calculate the level of complexity of these exercises, we base our approach on the effort required to solve them via informal proofs. We argue that such an effort, in turn, may be captured by formal proofs in cut-based tableaux that do not contain logical symbols. The rules utilized in these proofs are extracted by a mechanizable procedure we provide. We use the analytic character of such rules and the formal structure tableau proofs have to provide a computational procedure of the method in question. As case studies, we demonstrate how our method works with fragments of Set Theory and Number Theory. A prototype implementation of the method was also developed and we present it here.

COMMITTEE MEMBERS:
Presidente - 1517271 - JOAO MARCOS DE ALMEIDA
Interno - 1345816 - REGIVAN HUGO NUNES SANTIAGO
Externo ao Programa - 3884005 - PATRICK CESAR ALVES TERREMATTE - UFRNExterno à Instituição - CARLOS OLARTE
Externo à Instituição - ADOLFO GUSTAVO SERRA SECA NETO - UTFPR
Externa à Instituição - CLAUDIA NALON - UnB