| Campo DC | Valor | Lengua/Idioma |
|---|
| dc.contributor.advisor | Ayala-Rincón, Mauricio | pt_BR |
| dc.contributor.author | González Barragan, Andrés Felipe | pt_BR |
| dc.date.accessioned | 2026-02-27T13:30:05Z | - |
| dc.date.available | 2026-02-27T13:30:05Z | - |
| dc.date.issued | 2026-02-27 | - |
| dc.date.submitted | 2025-10-02 | - |
| dc.identifier.citation | GONZÁLEZ BARRAGAN, Andrés Felipe. Anti-unification in absorptive theories. 2025. 139 f., il. Tese (Doutorado em Matemática) — Universidade de Brasília, Brasília, 2025. | pt_BR |
| dc.identifier.uri | http://repositorio.unb.br/handle/10482/54148 | - |
| dc.description | Tese (doutorado) — Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Matemática, Programa de Pós-Graduação em Matemática, 2025. | pt_BR |
| dc.description.abstract | A anti-unificação consiste em determinar uma expressão que represente a estrutura comum
a duas expressões dadas, denominada generalização dessas expressões. O desenvolvimento
de procedimentos de anti-unificação para o cálculo de generalizações tem adquirido importância crescente em áreas como análise de programas, detecção de clones e raciocínio
simbólico. Enquanto os trabalhos iniciais se concentraram na anti-unificação sintática,
aplicações modernas frequentemente exigem raciocínio módulo teorias equacionais. Esta
tese dedica-se à anti-unificação em teorias absortivas, nas quais determinados símbolos de
operação “absortivos” satisfazem os axiomas f(εf , x) ≈ εf and f(x, εf ) ≈ εf para uma
constante “absorvente” relativa εf ; exemplos incluem multiplicação e zero, conjunção e
falso, interseção e conjunto vazio.
Neste trabalho são apresentadas ferramentas conceituais e um algoritmo correto para
anti-unificação modulo teorias absortivas, formalizado por meio de um conjunto de regras de inferência que transformam configurações, estruturas que codificam problemas
de anti-unificação e soluções parciais. São demonstradas propriedades de preservação das
configurações sob a aplicação das regras de inferência, garantindo a correção do algoritmo.
Uma contribuição central deste trabalho é o refinamento da análise de completude de um
algoritmo apresentado na 12ª International Joint Conference on Automated Reasoning
(2024). São identificadas generalizações adicionais não consideradas anteriormente, as
regras de inferência são melhoradas, e demonstra-se como as soluções correspondentes
podem ser calculadas a partir das configurações finais.
Esta tese também aborda teorias que podem incluir símbolos funcionais absortivos,
comutativos e absortivo-comutativos, que, para abreviar, chamamos de teorias absortivocomutativas. Propõe-se um novo conjunto de regras de inferência, acompanhado da prova
de correção do algoritmo resultante, estendendo a aplicabilidade da abordagem a estruturas de termos mais expressivas encontradas em cenários práticos. Além disso, é tratado o
caso restrito de anti-unificação para generalizações lineares, nas quais cada variável ocorre
no máximo uma vez nas soluções. O algoritmo é adaptado para o caso linear absortivo e
comutativo, provando-se sua correção e completude. No caso linear puramente absortivo,
o algoritmo computa um conjunto mínimo e completo de generalizações. | pt_BR |
| dc.language.iso | eng | pt_BR |
| dc.rights | Acesso Aberto | pt_BR |
| dc.title | Anti-unification in absorptive theories | pt_BR |
| dc.title.alternative | Anti-unificação em teorias absortivas | pt_BR |
| dc.type | Tese | pt_BR |
| dc.subject.keyword | Anti-unificação | pt_BR |
| dc.subject.keyword | Generalização (Matemática) | pt_BR |
| dc.subject.keyword | Teoria equacional | pt_BR |
| dc.subject.keyword | Dedução equacional | pt_BR |
| dc.subject.keyword | Teoria absortiva | pt_BR |
| dc.rights.license | A 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.unb.br, www.ibict.br, www.ndltd.org sem ressarcimento dos direitos autorais, de acordo com a Lei nº 9610/98, o texto integral da obra supracitada, 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. | pt_BR |
| dc.contributor.advisorco | Kutsia, Temur | pt_BR |
| dc.description.abstract1 | Anti-unification is the problem of finding an expression that captures the common structure of two given expressions. The resulting expression is called a generalization of them.
The development of anti-unification procedures, applied for computing generalizations
of expressions, has become increasingly important in applications such as program analysis, clone detection, and symbolic reasoning. While early work focused on syntactic
anti-unification, modern applications often require reasoning modulo equational theories.
This thesis focuses on anti-unification in absorptive theories, where certain “absorptive”
operation symbols satisfy the axioms f(εf , x) ≈ εf and f(x, εf ) ≈ εf for a relative “absorbing” constant εf ; e.g., multiplication and zero, conjunction and false, intersection and
empty set.
This thesis presents foundational tools and a sound algorithm for absorptive theories,
defined through a set of inference rules that transform configurations that are structures
encoding anti-unification problems and partial solutions. Preservation properties of the
configurations transformed by the inference rules are established, ensuring the soundness
of the algorithm. A key contribution of this work is the refinement of the completeness
analysis of an algorithm presented at the 12th International Joint Conference on Automated Reasoning (2024). Additional generalizations not previously considered are identified, the inference rules are enhanced, and it is shown how the corresponding solutions
can be computed from the final configurations. This thesis also addresses theories that
may include absorptive, commutative, and absorptive-commutative function symbols, for
short, absorptive commutative theories. A new set of inference rules is presented, and
the resulting algorithm is proved sound. This extends the applicability of the approach
to more expressive term structures encountered in practice. Additionally, the restricted
variant of anti-unification to linear generalizations, where each variable appears at most
once in the target solutions, is addressed. The algorithm is adapted for the linear absorptive commutative invariant, showing its soundness and completeness. In the linear
pure absorptive variant, the proposed algorithm computes a minimal and complete set of
generalizations. | pt_BR |
| dc.description.unidade | Instituto de Ciências Exatas (IE) | pt_BR |
| dc.description.unidade | Departamento de Matemática (IE MAT) | pt_BR |
| dc.description.ppg | Programa de Pós-Graduação em Matemática | pt_BR |
| Aparece en las colecciones: | Teses, dissertações e produtos pós-doutorado
|
