Nominal anti-unification with atom-variables

Registro completo de metadados
MetadadosDescriçãoIdioma
Autor(es): dc.contributorGoethe Universität, Frankfurt am Main-
Autor(es): dc.contributorImperial College London, Department of Computing-
Autor(es): dc.contributorUniversity of Brasília, Department of Mathematics-
Autor(es): dc.creatorSchmidt-Schauß, Manfred-
Autor(es): dc.creatorNantes Sobrinho, Daniele-
Data de aceite: dc.date.accessioned2024-07-22T12:02:24Z-
Data de disponibilização: dc.date.available2024-07-22T12:02:24Z-
Data de envio: dc.date.issued2023-07-10-
Data de envio: dc.date.issued2023-07-10-
Data de envio: dc.date.issued2021-
Fonte completa do material: dc.identifierhttp://repositorio2.unb.br/jspui/handle/10482/46038-
Fonte completa do material: dc.identifierhttps://orcid.org/0000-0001-8809-7385-
Fonte completa do material: dc.identifierhttps://orcid.org/0000-0002-1959-8730-
Fonte: dc.identifier.urihttp://educapes.capes.gov.br/handle/capes/794639-
Descrição: dc.descriptionAnti-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-
Descrição: dc.descriptionInstituto de Ciências Exatas (IE)-
Descrição: dc.descriptionDepartamento de Matemática (IE MAT)-
Formato: dc.formatapplication/pdf-
Idioma: dc.languageen-
Publicador: dc.publisherSchloss Dagstuhl – Leibniz-Zentrum f¨ur Informatik-
Direitos: dc.rightsAcesso Aberto-
Direitos: dc.rightsCreative Commons Attribution 4.0 license (CC BY 4.0)-
Palavras-chave: dc.subjectAnti-unificação-
Palavras-chave: dc.subjectAlgoritmos nominais-
Título: dc.titleNominal anti-unification with atom-variables-
Aparece nas coleções:Repositório Institucional – UNB

Não existem arquivos associados a este item.