A detailed study of bounded ACh-unification

Abstract

Esta dissertação trata do problema de unificação considerando a teoria equacional ACh, que consiste da teoria com um símbolo de função h que é homomorfismo sobre um operador associativo-comutativo. O problema de unificação módulo ACh busca em resolver equações do tipo s ?=ACh t, para termos de primeira ordem s e t, encontrando uma substituição θ que faz com que ambos os termos quando instanciados por esta substituição sejam iguais módulo ACh, i.e., tal que sθ =ACh tθ. Em geral, o problema de unificação módulo ACh é indecidível. Recentemente, Eeralla e Lynch definiram uma variação do problema chamada ACh-unificação com limitante que dá como entrada um limite na quantidade de símbolos de função de homomorfismo que são aplicados repetidamente, permitindo apenas soluções que não ultrapassem esse limite. Nosso objetivo é fornecer um estudo detalhado em ACh-unificação com limitantes, examinando cuidadosamente o algoritmo proposto para resolver o problema e verificando a prova de terminação, correção e completude.