Banca de DEFESA: Guilherme Borges Brandao

Uma banca de DEFESA de MESTRADO foi cadastrada pelo programa.
DISCENTE : Guilherme Borges Brandao
DATA : 06/03/2024
HORA: 16:00
LOCAL: PPGMAT
TÍTULO:

Um estudo detalhado em ACh-unificação com limitantes

PALAVRAS-CHAVES:

This dissertation deals with the unification problem regarding the associative-commutative equational theory with
homomorphism (ACh). This unification problem seeks to solve equations of the type , for first-order terms and , which
consists of finding a substitution that makes both terms when instantiated by this substitution identical, i.e., such that
. The unification modulo ACh problem consists of solving a similar problem but seeks substitutions such that both
instantiated terms are in the same ACh modulo equivalence class.
Past research established the undecidability of ACh Unification, defying the viability of finding solutions for this case.
However, recent work has introduced a new approach known as ‘Bounded ACh-Unification’. This new concept
strategically imposes a constraint by bounding the number of homomorphism function symbols occurring in a term.
With that, it was possible to define a set of inference rules and allegedly prove the correctness of the algorithm
defined by such rules. Our goal is to provide a comprehensive understanding of the procedure for solving the
bounded ACh-Unification problem by carefully examining its inference rules and validating the proof of termination,
soundness and completeness.

PÁGINAS: 53
RESUMO:

Esta dissertação trata do problema de unificação considerando a teoria equacional associativa-comutativa com
homomorfismo (ACh). O problema de unificação busca em resolver equações do tipo , para termos de primeira ordem
and , que consiste em encontrar uma substituição que faz com que ambos os termos quando instanciados por esta
substituição sejam idênticos, i.e., tal que . O problema de unificação módulo ACh consiste em resolver um problema
análogo, mas busca substituições tal que ambos os termos instanciados estejam na mesma classe de equivalência
módulo ACh.
Pesquisas anteriores estabeleceram a indecidibilidade do problema de unificação módulo ACh, desafiando a
viabilidade de encontrar soluções para este caso. No entanto, trabalhos recentes introduziram uma abordagem
diferenciada conhecida como Unificação ACh com limitante (do inglês `Bounded ACh Unification’) que impõe uma
restrição estratégica ao limitar a quantidade de símbolos de função de homomorfismo que ocorrem em um termo.
Com isso, foi possível definir um conjunto de regras de inferência para resolver problemas de unificação módulo ACh
com limitante e comprovar a correção do algoritmo definido por tais regras. Nosso objetivo é fornecer uma
compreensão abrangente do método para resolver o problema de unificação ACh com limitante, examinando
cuidadosamente as regras de inferência e validando a prova de terminação, correção e completude.

MEMBROS DA BANCA:
Presidente - 1151467 - DANIELE NANTES SOBRINHO
Externo ao Programa - 2315320 - FLAVIO LEONARDO CAVALCANTI DE MOURA - nullInterno - 2180096 - MAURICIO AYALA RINCON
Externa à Instituição - THAYNARA ARIELLY DE LIMA - UFG