Repository logo
  • Log In
    Log in via Symplectic to deposit your publication(s).
Repository logo
  • About
  • Communities & Collections
  • Advanced Search
  • Statistics
  • Log In
    Log in via Symplectic to deposit your publication(s).
  1. Home
  2. Faculty of Engineering
  3. Faculty of Engineering
  4. Nominal anti-unification with atom-variables
 
  • Details
Nominal anti-unification with atom-variables
File(s)
LIPIcs-FSCD-2022-7.pdf (903.19 KB)
Published version
Author(s)
Schmidt-Schauß, Manfred
Nantes Sobrinho, Daniele
Type
Conference Paper
Abstract
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.
Date Issued
2022-06-28
Date Acceptance
2022-04-16
Citation
LIPIcs : Leibniz International Proceedings in Informatics, 2022, 228, pp.7:1-7:22
URI
http://hdl.handle.net/10044/1/110009
DOI
https://www.dx.doi.org/10.4230/LIPIcs.FSCD.2022.7
ISSN
1868-8969
Publisher
Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
Start Page
7:1
End Page
7:22
Journal / Book Title
LIPIcs : Leibniz International Proceedings in Informatics
Volume
228
Copyright Statement
© Manfred Schmidt-Schaußand Daniele Nantes-Sobrinho;
licensed under Creative Commons License CC-BY 4.0 (https://creativecommons.org/licenses/by/4.0/)
License URL
Attribution 4.0 International
Source
Formal Structures for Computation and Deduction
Publication Status
Published
Start Date
2022-06-02
Finish Date
2022-08-05
Coverage Spatial
Haifa, Israel
About
Spiral Depositing with Spiral Publishing with Spiral Symplectic
Contact us
Open access team Report an issue
Other Services
Scholarly Communications Library Services
logo

Imperial College London

South Kensington Campus

London SW7 2AZ, UK

tel: +44 (0)20 7589 5111

Accessibility Modern slavery statement Cookie Policy

Built with DSpace-CRIS software - Extension maintained and optimized by 4Science

  • Cookie settings
  • Privacy policy
  • End User Agreement
  • Send Feedback