2026-07-23T18:08:57Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16288 2024-03-12T12:00:45Z ddc:004 open_access

Nominal Anti-Unification with Atom-Variables Schmidt-Schauß, Manfred Nantes-Sobrinho, Daniele Generalization anti-unification nominal algorithms higher-order deduction 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: NL_A-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 NL_A-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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Manfred Schmidt-Schauß and Daniele Nantes-Sobrinho 2022 Is Part Of LIPIcs, Volume 228, 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2022.7 urn:nbn:de:0030-drops-162885 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2022.7 eng https://creativecommons.org/licenses/by/4.0/legalcode