Banca de DEFESA: Guilherme Borges Brandao

Uma banca de DEFESA de MESTRADO foi cadastrada pelo programa.
STUDENT : Guilherme Borges Brandao
DATE: 06/03/2024
TIME: 16:00
LOCAL: PPGMAT
TITLE:

A detailed study of ACh-unification

KEY WORDS:

unification, equational theories, associativity-commutativity, homomorphism

PAGES: 53
BIG AREA: Ciências Exatas e da Terra
AREA: Matemática
SUMMARY:

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.

COMMITTEE MEMBERS:
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