Banca de DEFESA: Gabriel Ferreira Silva

Uma banca de DEFESA de DOUTORADO foi cadastrada pelo programa.
DISCENTE : Gabriel Ferreira Silva
DATA : 22/02/2024
HORA: 10:00
LOCAL: Laboratório LaForCE Prédio CIC/EST
TÍTULO:

Rumo à unificação nominal AC

PALAVRAS-CHAVES:

Métodos Formais, PVS, Lógica Nominal, Unificação, Unificação AC, C-Matching

PÁGINAS: 130
RESUMO:

O paradigma nominal estende a sintaxe de primeira ordem e representa adequadamente
o conceito de variáveis ligadas. Para trabalhar com esse vantajoso paradigma faz-se ne-
cessário adaptar noções de primeira ordem a ele, como unificação e matching. Esta tese
é sobre unificação e matching no paradigma nominal na presença de uma teoria equaci-
onal E e sobre nosso trabalho em progresso para obter um algoritmo de AC-unificação
nominal. Inicialmente, generalizamos um algoritmo de C-unificação nominal para realizar
também matching e equality-checking e formalizamos o algoritmo generalizado. Isto foi
feito por meio da adição de um parâmetro X para lidar com variáveis protegidas e a
formalização foi usado para testar uma implementação manual em Python do algoritmo.
Em seguida, como um primeiro passo em direção a AC-unificação nominal, fornecemos a
primeira formalização de um algoritmo de AC-unificação em primeira ordem. Escolhemos
formalizar o algoritmo seminal de Stickel. A prova de terminação utiliza uma intrincada
(mas devidamente motivada) medida lexicográfica, que está baseada na demonstração de
terminação dada por Fages. Depois disso, adaptamos o algoritmo de AC-unificação em
primeira ordem para obter o primeiro algoritmo para AC-matching em nominal e verifica-
mos que o algoritmo termina e é correto e completo. Assim como fizemos em C-unificação
nominal, usamos um parâmetro X para as variáveis protegidas e essa abordagem nos per-
mitiu obter um AC-equality-checker como corolário. As 3 formalizações descritas foram
feitas no assistente de provas PVS e integram a NASALib, o principal repositório de for-
malizações do PVS. Para cada uma dessas formalizações nós descrevemos os arquivos que
compõem a formalização, detalhando a estrutura, hierarquia e tamanho. Não foi possível
propor um algoritmo de AC-unificação nominal, mas mostramos que o problema tem duas
questões interessantes associadas a ele: gerar as soluções para π · X ≈? X e demonstrar
terminação. Para a primeira questão, propomos um procedimento não determinístico de
enumeração e exemplificamos como este calcula soluções não triviais. Para a segunda
questão demonstramos como o problema f (X, W ) ≈? f (π · X, π · Y ) gera um loop e prova-
mos que é suficiente entrar no loop uma quantidade limitada de vezes, onde esse limite
depende da ordem da permutação π. Infelizmente, não fomos capazes de generalizar nosso
raciocínio para problemas semelhantes.

MEMBROS DA BANCA:
Externo à Instituição - CHRISTIAN URBAN
Externo à Instituição - JOSÉ MESEGUER
Externo à Instituição - CÉSAR MUÑOZ
Presidente - 2180096 - MAURICIO AYALA RINCON
Interno - 1702036 - VANDER RAMOS ALVES