Skip navigation
Use este identificador para citar ou linkar para este item: http://repositorio.unb.br/handle/10482/46038
Arquivos associados a este item:
Arquivo Descrição TamanhoFormato 
EVENTO_NominalAntiUnification.pdf903,19 kBAdobe PDFVisualizar/Abrir
Registro completo de metadados
Campo DCValorIdioma
dc.contributor.authorSchmidt-Schauß, Manfred-
dc.contributor.authorNantes Sobrinho, Daniele-
dc.date.accessioned2023-07-10T11:41:53Z-
dc.date.available2023-07-10T11:41:53Z-
dc.date.issued2022-
dc.identifier.citationSCHMIDT-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.urihttp://repositorio2.unb.br/jspui/handle/10482/46038-
dc.language.isoengpt_BR
dc.publisherSchloss Dagstuhl – Leibniz-Zentrum f¨ur Informatikpt_BR
dc.rightsAcesso Abertopt_BR
dc.titleNominal anti-unification with atom-variablespt_BR
dc.typeTrabalho apresentado em eventopt_BR
dc.subject.keywordAnti-unificaçãopt_BR
dc.subject.keywordAlgoritmos nominaispt_BR
dc.rights.licenseCreative Commons Attribution 4.0 license (CC BY 4.0)pt_BR
dc.identifier.doi10.4230/LIPIcs.FSCD.2022.7pt_BR
dc.description.abstract1Anti-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 generalizationpt_BR
dc.identifier.orcidhttps://orcid.org/0000-0001-8809-7385pt_BR
dc.identifier.orcidhttps://orcid.org/0000-0002-1959-8730pt_BR
dc.contributor.affiliationGoethe Universität, Frankfurt am Mainpt_BR
dc.contributor.affiliationImperial College London, Department of Computingpt_BR
dc.contributor.affiliationUniversity of Brasília, Department of Mathematicspt_BR
dc.description.unidadeInstituto de Ciências Exatas (IE)pt_BR
dc.description.unidadeDepartamento de Matemática (IE MAT)pt_BR
Aparece nas coleções:Trabalhos apresentados em evento

Mostrar registro simples do item Visualizar estatísticas



Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.