Banca de DEFESA: MARIA JULIA DIAS LIMA

Uma banca de DEFESA de MESTRADO foi cadastrada pelo programa.
DISCENTE : MARIA JULIA DIAS LIMA
DATA : 27/08/2026
HORA: 09:00
LOCAL: Remoto
TÍTULO:

Formalização de Algoritmos de Antiunificação em PVS

PALAVRAS-CHAVES:

Antiunificação, raciocínio automatizado, raciocínio equacional, prova interativa de teoremas, Prototype Verification System (PVS)

PÁGINAS: 100
RESUMO:

Antiunificação é o problema de encontrar um termo que represente a
estrutura mais comum entre dois outros termos. Isto é, construir um termo r
que descreva as semelhanças entre dois outros termos, s e t, tal que
existam substituições que mapeiem r para s e r para t. Este termo é chamado
de "generalizador menos geral" (least general generalizer) dos termos s e
t. Esse problema foi investigado pela primeira vez por Plotkin e Reynolds e
publicado em "Machine Intelligence" em 1970. Soluções algorítmicas do
problema de antiunificação são amplamente utilizadas hoje em problemas
computacionais relacionados à detecção de clonagem de código, à detecção e
correção de erros e a melhorias em compilações paralelas. O trabalho
apresentado nesta dissertação concentra-se em verificar algoritmos de
antiunificação no "Prototype Verification System" (PVS).
São considerados os casos de antiunificação sintática e antiunificação na
presença de operadores comutativos, especificando algoritmos funcionais
baseados em regras de inferência, concebidos para construir generalizadores
menos gerais. É apresentada uma formalização do problema, comprovando sua
correção no caso sintático, conforme apresentado no "17th NASA Formal
Methods Symposium" (NFM 2025), que marca a primeira verificação
mecanizada desse tipo para esse problema. O trabalho também identifica os
problemas existentes nas provas de completude que constituíam o estado da
arte quando a formalização da mesma foi abordada e fornece uma solução
teórica para esses problemas, apresentada em "Logical Frameworks and
Meta-Languages: Theory and Practice" (LFMTP 2026). Por fim, o documento
inclui um esboço da formalização da correção considerando o caso comutativo.

MEMBROS DA BANCA:
Externo à Instituição - CÉSAR MUÑOZ - NASA
Externa ao Programa - 1151467 - DANIELE NANTES SOBRINHO - nullPresidente - ***.627.171-** - MAURICIO AYALA RINCON - UB
Interno - 1702036 - VANDER RAMOS ALVES