Banca de QUALIFICAÇÃO: MARIA JULIA DIAS LIMA

Uma banca de QUALIFICAÇÃO de MESTRADO foi cadastrada pelo programa.
DISCENTE : MARIA JULIA DIAS LIMA
DATA : 29/08/2025
HORA: 09:00
LOCAL: LaForCE Prédio CIC/EST UnB
TÍTULO:

Formalização de Anti-unificação Comutativa em PVS

PALAVRAS-CHAVES:

Raciocínio Equacional, Unificação, Antiunificação, Prova de Teoremas, Provadores Interativos de Teoremas, PVS

PÁGINAS: 50
RESUMO:

Antiunificação é um problema que começou a ser explorado em 1970 com o trabalho de Plotkin e Reynolds, e consiste em encontrar um termo comum r entre outras outros dois termos, s e t, tal que existam substituições sigma e rho tal que sigma(r) = s e $rho(r) = t sejam verdade. Isso é chamado de um generalizador dos termos s e t. No algoritmo utilizado nesse trabalho, não apenas um generalizador é encontrado, mas é o generalizador menos geral entre os termos dados.

Desde então, evoluções consideráveis foram feitas nesse problema e tem sido desenvolvido para uso em um número considerável de situações. Ele não foi, no entanto, formalizado em um assistente de provas no contexto sintático de primeira-ordem. Este trabalho busca apresentar uma formalização da antiunificação sintática de primeira ordem usando o assistente de provas PVS. A prova é baseada no trabalho feito previamente para o problema dual de unificação, formalizado para o contexto nominal.

MEMBROS DA BANCA:
Presidente - 2180096 - MAURICIO AYALA RINCON
Interno - 1702036 - VANDER RAMOS ALVES
Externa à Instituição - THAYNARA ARIELLY DE LIMA - UFG