A detailed study of bounded ACh-unification

Registro completo de metadados
MetadadosDescriçãoIdioma
Autor(es): dc.contributorNantes Sobrinho, Daniele-
Autor(es): dc.creatorBrandão, Guilherme Borges-
Data de aceite: dc.date.accessioned2024-10-23T15:05:57Z-
Data de disponibilização: dc.date.available2024-10-23T15:05:57Z-
Data de envio: dc.date.issued2024-08-06-
Data de envio: dc.date.issued2024-08-06-
Data de envio: dc.date.issued2024-08-06-
Data de envio: dc.date.issued2024-03-06-
Fonte completa do material: dc.identifierhttp://repositorio2.unb.br/jspui/handle/10482/49595-
Fonte: dc.identifier.urihttp://educapes.capes.gov.br/handle/capes/874256-
Descrição: dc.descriptionDissertação (mestrado) — Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, 2024.-
Descrição: dc.descriptionEsta 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.-
Descrição: dc.descriptionThis master’s thesis deals with the unification problem regarding the equational theory ACh, which consists of the theory with a function symbol h that is an homomorphism over an associative-commutative operator. The Unification problem modulo ACh seeks to solve equations of the type s ?=ACh t, for first-order terms s and t, finding a substitution θ that makes both terms, when instantiated by this substitution, equal modulo ACh, i.e., such that sθ =ACh tθ. In general, the problem of ACh Unification is undecidable. Recently, Eeralla and Lynch defined a variation of the problem called Bounded ACh Unification, which gives as an input a bound on the number of homomorphism function symbols that are applied repeatedly, allowing only solutions that do not surpass such bound. Our goal is to provide a detailed study of Bounded ACh Unification by carefully examining the algorithm designed to solve the problem and validating the proof of termination, soundness and completeness.-
Descrição: dc.descriptionInstituto de Ciências Exatas (IE)-
Descrição: dc.descriptionDepartamento de Matemática (IE MAT)-
Descrição: dc.descriptionPrograma de Pós-Graduação em Matemática-
Formato: dc.formatapplication/pdf-
Idioma: dc.languageen-
Direitos: dc.rightsAcesso Aberto-
Direitos: dc.rightsA concessão da licença deste item refere-se ao termo de autorização impresso assinado pelo autor com as seguintes condições: Na qualidade de titular dos direitos de autor da publicação, autorizo a Universidade de Brasília e o IBICT a disponibilizar por meio dos sites www.bce.unb.br, www.ibict.br, http://hercules.vtls.com/cgi-bin/ndltd/chameleon?lng=pt&skin=ndltd sem ressarcimento dos direitos autorais, de acordo com a Lei nº 9610/98, o texto integral da obra disponibilizada, conforme permissões assinaladas, para fins de leitura, impressão e/ou download, a título de divulgação da produção científica brasileira, a partir desta data.-
Palavras-chave: dc.subjectTeorias equacionais-
Palavras-chave: dc.subjectAssociatividade-
Palavras-chave: dc.subjectComutatividade-
Título: dc.titleA detailed study of bounded ACh-unification-
Tipo de arquivo: dc.typelivro digital-
Aparece nas coleções:Repositório Institucional – UNB

Não existem arquivos associados a este item.