| Campo DC | Valor | Idioma |
|---|
| dc.contributor.author | Schmidt-Schauß, Manfred | - |
| dc.contributor.author | Nantes Sobrinho, Daniele | - |
| dc.date.accessioned | 2023-07-10T11:41:53Z | - |
| dc.date.available | 2023-07-10T11:41:53Z | - |
| dc.date.issued | 2022 | - |
| dc.identifier.citation | SCHMIDT-SCHAUß, Manfred; NANTES-SOBRINHO, Daniele. Nominal anti-unification with atom-variables. In: INTERNATIONAL CONFERENCE ON FORMAL STRUCTURES FOR COMPUTATION AND DEDUCTION (FSCD 2022), 7th, v. 228, 2022. Dagstuhl, Germany: Leibniz International Proceedings in Informatics (LIPIcs), 2022, p. 1-22. DOI: 10.4230/LIPIcs.FSCD.2022.7. Disponível em: https://drops.dagstuhl.de/opus/volltexte/2022/16288/pdf/LIPIcs-FSCD-2022-7.pdf. Acesso em: 09 jul. 2023. | pt_BR |
| dc.identifier.uri | http://repositorio2.unb.br/jspui/handle/10482/46038 | - |
| dc.language.iso | eng | pt_BR |
| dc.publisher | Schloss Dagstuhl – Leibniz-Zentrum f¨ur Informatik | pt_BR |
| dc.rights | Acesso Aberto | pt_BR |
| dc.title | Nominal anti-unification with atom-variables | pt_BR |
| dc.type | Trabalho apresentado em evento | pt_BR |
| dc.subject.keyword | Anti-unificação | pt_BR |
| dc.subject.keyword | Algoritmos nominais | pt_BR |
| dc.rights.license | Creative Commons Attribution 4.0 license (CC BY 4.0) | pt_BR |
| dc.identifier.doi | 10.4230/LIPIcs.FSCD.2022.7 | pt_BR |
| dc.description.abstract1 | Anti-unification is the task of generalizing a set of expressions in the most specific way. It was
extended to the nominal framework by Baumgarter, Kutsia, Levy and Villaret, who defined an
algorithm solving the nominal anti-unification problem, which runs in polynomial time. Unfortunately,
when an infinite set of atoms are allowed in generalizations, a minimal complete set of solutions in
nominal anti-unification does not exist, in general. In this paper, we present a more general approach
to nominal anti-unification that uses atom-variables instead of explicit atoms, and two variants
of freshness constraints: NLA-constraints (with atom-variables), and Eqr-constraints based on
Equivalence relations on atom-variables. The idea of atom-variables is that different atom-variables
may be instantiated with identical or different atoms. Albeit simple, this freedom in the formulation
increases its application potential: we provide an algorithm that is finitary for the NLA-freshness
constraints, and for Eqr-freshness constraints it computes a unique least general generalization.
There is a price to pay in the general case: checking freshness constraints and other related logical
questions will require exponential time. The setting of Baumgartner et al. is improved by the
atom-only case, which runs in polynomial time and computes a unique least general generalization | pt_BR |
| dc.identifier.orcid | https://orcid.org/0000-0001-8809-7385 | pt_BR |
| dc.identifier.orcid | https://orcid.org/0000-0002-1959-8730 | pt_BR |
| dc.contributor.affiliation | Goethe Universität, Frankfurt am Main | pt_BR |
| dc.contributor.affiliation | Imperial College London, Department of Computing | pt_BR |
| dc.contributor.affiliation | University of Brasília, Department of Mathematics | pt_BR |
| dc.description.unidade | Instituto de Ciências Exatas (IE) | pt_BR |
| dc.description.unidade | Departamento de Matemática (IE MAT) | pt_BR |
| Aparece nas coleções: | Trabalhos apresentados em evento
|
