Search Results

Documents authored by Kutsia, Temur

Document
Complete Volume
DOI: 10.4230/LIPIcs.ITP.2024
LIPIcs, Volume 309, ITP 2024, Complete Volume

Authors: Yves Bertot, Temur Kutsia, and Michael Norrish

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
LIPIcs, Volume 309, ITP 2024, Complete Volume
Cite as

15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 1-714, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Proceedings{bertot_et_al:LIPIcs.ITP.2024,
  title =	{{LIPIcs, Volume 309, ITP 2024, Complete Volume}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{1--714},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024},
  URN =		{urn:nbn:de:0030-drops-207277},
  doi =		{10.4230/LIPIcs.ITP.2024},
  annote =	{Keywords: LIPIcs, Volume 309, ITP 2024, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.ITP.2024.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Yves Bertot, Temur Kutsia, and Michael Norrish

Published in: LIPIcs, Volume 309, 15th International Conference on Interactive Theorem Proving (ITP 2024)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 0:i-0:xii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{bertot_et_al:LIPIcs.ITP.2024.0,
  author =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{15th International Conference on Interactive Theorem Proving (ITP 2024)},
  pages =	{0:i--0:xii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-337-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{309},
  editor =	{Bertot, Yves and Kutsia, Temur and Norrish, Michael},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2024.0},
  URN =		{urn:nbn:de:0030-drops-207287},
  doi =		{10.4230/LIPIcs.ITP.2024.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2020.26
Unital Anti-Unification: Type and Algorithms

Authors: David M. Cerna and Temur Kutsia

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
Unital equational theories are defined by axioms that assert the existence of the unit element for some function symbols. We study anti-unification (AU) in unital theories and address the problems of establishing generalization type and designing anti-unification algorithms. First, we prove that when the term signature contains at least two unital functions, anti-unification is of the nullary type by showing that there exists an AU problem, which does not have a minimal complete set of generalizations. Next, we consider two special cases: the linear variant and the fragment with only one unital symbol, and design AU algorithms for them. The algorithms are terminating, sound, complete, and return tree grammars from which the set of generalizations can be constructed. Anti-unification for both special cases is finitary. Further, the algorithm for the one-unital fragment is extended to the unrestricted case. It terminates and returns a tree grammar which produces an infinite set of generalizations. At the end, we discuss how the nullary type of unital anti-unification might affect the anti-unification problem in some combined theories, and list some open questions.
Cite as

David M. Cerna and Temur Kutsia. Unital Anti-Unification: Type and Algorithms. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{cerna_et_al:LIPIcs.FSCD.2020.26,
  author =	{Cerna, David M. and Kutsia, Temur},
  title =	{{Unital Anti-Unification: Type and Algorithms}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{26:1--26:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.26},
  URN =		{urn:nbn:de:0030-drops-123482},
  doi =		{10.4230/LIPIcs.FSCD.2020.26},
  annote =	{Keywords: Anti-unification, tree grammars, unital theories, collapse theories}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2020.30
Constraint Solving over Multiple Similarity Relations

Authors: Besik Dundua, Temur Kutsia, Mircea Marin, and Cleopatra Pau

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

Abstract
Similarity relations are reflexive, symmetric, and transitive fuzzy relations. They help to make approximate inferences, replacing the notion of equality. Similarity-based unification has been quite intensively investigated, as a core computational method for approximate reasoning and declarative programming. In this paper we consider solving constraints over several similarity relations, instead of a single one. Multiple similarities pose challenges to constraint solving, since we can not rely on the transitivity property anymore. Existing methods for unification with fuzzy proximity relations (reflexive, symmetric, non-transitive relations) do not provide a solution that would adequately reflect particularities of dealing with multiple similarities. To address this problem, we develop a constraint solving algorithm for multiple similarity relations, prove its termination, soundness, and completeness properties, and discuss applications.
Cite as

Besik Dundua, Temur Kutsia, Mircea Marin, and Cleopatra Pau. Constraint Solving over Multiple Similarity Relations. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 30:1-30:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{dundua_et_al:LIPIcs.FSCD.2020.30,
  author =	{Dundua, Besik and Kutsia, Temur and Marin, Mircea and Pau, Cleopatra},
  title =	{{Constraint Solving over Multiple Similarity Relations}},
  booktitle =	{5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
  pages =	{30:1--30:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-155-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{167},
  editor =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.30},
  URN =		{urn:nbn:de:0030-drops-123522},
  doi =		{10.4230/LIPIcs.FSCD.2020.30},
  annote =	{Keywords: Fuzzy relations, similarity, constraint solving}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2019.10
A Generic Framework for Higher-Order Generalizations

Authors: David M. Cerna and Temur Kutsia

Published in: LIPIcs, Volume 131, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)

Abstract
We consider a generic framework for anti-unification of simply typed lambda terms. It helps to compute generalizations which contain maximally common top part of the input expressions, without nesting generalization variables. The rules of the corresponding anti-unification algorithm are formulated, and their soundness and termination are proved. The algorithm depends on a parameter which decides how to choose terms under generalization variables. Changing the particular values of the parameter, we obtained four new unitary variants of higher-order anti-unification and also showed how the already known pattern generalization fits into the schema.
Cite as

David M. Cerna and Temur Kutsia. A Generic Framework for Higher-Order Generalizations. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 131, pp. 10:1-10:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{cerna_et_al:LIPIcs.FSCD.2019.10,
  author =	{Cerna, David M. and Kutsia, Temur},
  title =	{{A Generic Framework for Higher-Order Generalizations}},
  booktitle =	{4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)},
  pages =	{10:1--10:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-107-8},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{131},
  editor =	{Geuvers, Herman},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2019.10},
  URN =		{urn:nbn:de:0030-drops-105175},
  doi =		{10.4230/LIPIcs.FSCD.2019.10},
  annote =	{Keywords: anti-unification, typed lambda calculus, least general generalization}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.9
Term-Graph Anti-Unification

Authors: Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
We study anti-unification for possibly cyclic, unranked term-graphs and develop an algorithm, which computes a minimal complete set of generalizations for them. For bisimilar graphs the algorithm computes the join in the lattice generated by a functional bisimulation. These results generalize anti-unification for ranked and unranked terms to the corresponding term-graphs, and solve also anti-unification problems for rational terms and dags. Our results open a way to widen anti-unification based code clone detection techniques from a tree representation to a graph representation of the code.
Cite as

Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. Term-Graph Anti-Unification. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 9:1-9:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{baumgartner_et_al:LIPIcs.FSCD.2018.9,
  author =	{Baumgartner, Alexander and Kutsia, Temur and Levy, Jordi and Villaret, Mateu},
  title =	{{Term-Graph Anti-Unification}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{9:1--9:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.9},
  URN =		{urn:nbn:de:0030-drops-91797},
  doi =		{10.4230/LIPIcs.FSCD.2018.9},
  annote =	{Keywords: Cyclic term-graps, anti-unification, least general generalization}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2018.12
Higher-Order Equational Pattern Anti-Unification

Authors: David M. Cerna and Temur Kutsia

Published in: LIPIcs, Volume 108, 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)

Abstract
We consider anti-unification for simply typed lambda terms in associative, commutative, and associative-commutative theories and develop a sound and complete algorithm which takes two lambda terms and computes their generalizations in the form of higher-order patterns. The problem is finitary: the minimal complete set of generalizations contains finitely many elements. We define the notion of optimal solution and investigate special fragments of the problem for which the optimal solution can be computed in linear or polynomial time.
Cite as

David M. Cerna and Temur Kutsia. Higher-Order Equational Pattern Anti-Unification. In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{cerna_et_al:LIPIcs.FSCD.2018.12,
  author =	{Cerna, David M. and Kutsia, Temur},
  title =	{{Higher-Order Equational Pattern Anti-Unification}},
  booktitle =	{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)},
  pages =	{12:1--12:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-077-4},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{108},
  editor =	{Kirchner, H\'{e}l\`{e}ne},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2018.12},
  URN =		{urn:nbn:de:0030-drops-91826},
  doi =		{10.4230/LIPIcs.FSCD.2018.12},
  annote =	{Keywords: Simply typed lambda calculus, anti-unification, equational theories}
}
Document
DOI: 10.4230/OASIcs.ICLP.2016.10
P-rho-Log: Combining Logic Programming with Conditional Transformation Systems

Authors: Besik Dundua, Temur Kutsia, and Klaus Reisenberger-Hagmayer

Published in: OASIcs, Volume 52, Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016)

Abstract
P-rho-Log extends Prolog by conditional transformations that are controlled by strategies. We give a brief overview of the tool and illustrate its capabilities.
Cite as

Besik Dundua, Temur Kutsia, and Klaus Reisenberger-Hagmayer. P-rho-Log: Combining Logic Programming with Conditional Transformation Systems. In Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016). Open Access Series in Informatics (OASIcs), Volume 52, pp. 10:1-10:5, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{dundua_et_al:OASIcs.ICLP.2016.10,
  author =	{Dundua, Besik and Kutsia, Temur and Reisenberger-Hagmayer, Klaus},
  title =	{{P-rho-Log: Combining Logic Programming with Conditional Transformation Systems}},
  booktitle =	{Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016)},
  pages =	{10:1--10:5},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-007-1},
  ISSN =	{2190-6807},
  year =	{2016},
  volume =	{52},
  editor =	{Carro, Manuel and King, Andy and Saeedloei, Neda and De Vos, Marina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICLP.2016.10},
  URN =		{urn:nbn:de:0030-drops-67409},
  doi =		{10.4230/OASIcs.ICLP.2016.10},
  annote =	{Keywords: Conditional transformation rules, strategies, Prolog}
}
Document
DOI: 10.4230/LIPIcs.RTA.2015.57
Nominal Anti-Unification

Authors: Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Abstract
We study nominal anti-unification, which is concerned with computing least general generalizations for given terms-in-context. In general, the problem does not have a least general solution, but if the set of atoms permitted in generalizations is finite, then there exists a least general generalization which is unique modulo variable renaming and alpha-equivalence. We present an algorithm that computes it. The algorithm relies on a subalgorithm that constructively decides equivariance between two terms-in-context. We prove soundness and completeness properties of both algorithms and analyze their complexity. Nominal anti-unification can be applied to problems where generalization of first-order terms is needed (inductive learning, clone detection, etc.), but bindings are involved.
Cite as

Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. Nominal Anti-Unification. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 57-73, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{baumgartner_et_al:LIPIcs.RTA.2015.57,
  author =	{Baumgartner, Alexander and Kutsia, Temur and Levy, Jordi and Villaret, Mateu},
  title =	{{Nominal Anti-Unification}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{57--73},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.57},
  URN =		{urn:nbn:de:0030-drops-51895},
  doi =		{10.4230/LIPIcs.RTA.2015.57},
  annote =	{Keywords: Nominal Anti-Unification, Term-in-context, Equivariance}
}
Document
DOI: 10.4230/LIPIcs.RTA.2015.241
Constructing Orthogonal Designs in Powers of Two: Gröbner Bases Meet Equational Unification

Authors: Ilias Kotsireas, Temur Kutsia, and Dimitris E. Simos

Published in: LIPIcs, Volume 36, 26th International Conference on Rewriting Techniques and Applications (RTA 2015)

Abstract
In the past few decades, design theory has grown to encompass a wide variety of research directions. It comes as no surprise that applications in coding theory and communications continue to arise, and also that designs have found applications in new areas. Computer science has provided a new source of applications of designs, and simultaneously a field of new and challenging problems in design theory. In this paper, we revisit a construction for orthogonal designs using the multiplication tables of Cayley-Dickson algebras of dimension $2^n$. The desired orthogonal designs can be described by a system of equations with the aid of a Groebner basis computation. For orders greater than 16 the combinatorial explosion of the problem gives rise to equations that are unfeasible to be handled by traditional search algorithms. However, the structural properties of the designs make this problem possible to be tackled in terms of rewriting techniques, by equational unification. We establish connections between central concepts of design theory and equational unification where equivalence operations of designs point to the computation of a minimal complete set of unifiers. These connections make viable the computation of some types of orthogonal designs that have not been found before with the aforementioned algebraic modelling.
Cite as

Ilias Kotsireas, Temur Kutsia, and Dimitris E. Simos. Constructing Orthogonal Designs in Powers of Two: Gröbner Bases Meet Equational Unification. In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 241-256, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{kotsireas_et_al:LIPIcs.RTA.2015.241,
  author =	{Kotsireas, Ilias and Kutsia, Temur and Simos, Dimitris E.},
  title =	{{Constructing Orthogonal Designs in Powers of Two: Gr\"{o}bner Bases Meet Equational Unification}},
  booktitle =	{26th International Conference on Rewriting Techniques and Applications (RTA 2015)},
  pages =	{241--256},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-85-9},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{36},
  editor =	{Fern\'{a}ndez, Maribel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.241},
  URN =		{urn:nbn:de:0030-drops-52006},
  doi =		{10.4230/LIPIcs.RTA.2015.241},
  annote =	{Keywords: Orthogonal designs, unification theory, algorithms, Groebner bases}
}
Document
DOI: 10.4230/LIPIcs.RTA.2013.113
A Variant of Higher-Order Anti-Unification

Authors: Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret

Published in: LIPIcs, Volume 21, 24th International Conference on Rewriting Techniques and Applications (RTA 2013)

Abstract
We present a rule-based Huet's style anti-unification algorithm for simply-typed lambda-terms in eta-long beta-normal form, which computes a least general higher-order pattern generalization. For a pair of arbitrary terms of the same type, such a generalization always exists and is unique modulo alpha-equivalence and variable renaming. The algorithm computes it in cubic time within linear space. It has been implemented and the code is freely available.
Cite as

Alexander Baumgartner, Temur Kutsia, Jordi Levy, and Mateu Villaret. A Variant of Higher-Order Anti-Unification. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 113-127, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{baumgartner_et_al:LIPIcs.RTA.2013.113,
  author =	{Baumgartner, Alexander and Kutsia, Temur and Levy, Jordi and Villaret, Mateu},
  title =	{{A Variant of Higher-Order Anti-Unification}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{113--127},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{van Raamsdonk, Femke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2013.113},
  URN =		{urn:nbn:de:0030-drops-40579},
  doi =		{10.4230/LIPIcs.RTA.2013.113},
  annote =	{Keywords: higher-order anti-unification, higher-order patterns}
}
Document
DOI: 10.4230/LIPIcs.RTA.2011.219
Anti-Unification for Unranked Terms and Hedges

Authors: Temur Kutsia, Jordi Levy, and Mateu Villaret

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

Abstract
We study anti-unification for unranked terms and hedges that may contain term and hedge variables. The anti-unification problem of two hedges ~s_1 and ~s_2 is concerned with finding their generalization, a hedge ~q such that both ~s_1 and ~s_2 are instances of ~q under some substitutions. Hedge variables help to fill in gaps in generalizations, while term variables abstract single (sub)terms with different top function symbols. First, we design a complete and minimal algorithm to compute least general generalizations. Then, we improve the efficiency of the algorithm by restricting possible alternatives permitted in the generalizations. The restrictions are imposed with the help of a rigidity function that is a parameter in the improved algorithm and selects certain common subsequences from the hedges to be generalized. Finally, we indicate a possible application of the algorithm in software engineering.
Cite as

Temur Kutsia, Jordi Levy, and Mateu Villaret. Anti-Unification for Unranked Terms and Hedges. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 219-234, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{kutsia_et_al:LIPIcs.RTA.2011.219,
  author =	{Kutsia, Temur and Levy, Jordi and Villaret, Mateu},
  title =	{{Anti-Unification for Unranked Terms and Hedges}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{219--234},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.219},
  URN =		{urn:nbn:de:0030-drops-31181},
  doi =		{10.4230/LIPIcs.RTA.2011.219},
  annote =	{Keywords: Anti-unification, generalization, unranked terms, hedges, software clones.}
}
Document
DOI: 10.4230/LIPIcs.RTA.2010.193
Order-Sorted Unification with Regular Expression Sorts

Authors: Temur Kutsia and Mircea Marin

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract
We extend first-order order-sorted unification by permitting regular expression sorts for variables and in the domains of function symbols. The set of basic sorts is finite. The obtained signature corresponds to a finite bottom-up hedge automaton. The unification problem in such a theory generalizes some known unification problems. Its unification type is infinitary. We give a complete unification procedure and prove decidability.
Cite as

Temur Kutsia and Mircea Marin. Order-Sorted Unification with Regular Expression Sorts. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 193-208, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{kutsia_et_al:LIPIcs.RTA.2010.193,
  author =	{Kutsia, Temur and Marin, Mircea},
  title =	{{Order-Sorted Unification with Regular Expression Sorts}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{193--208},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.193},
  URN =		{urn:nbn:de:0030-drops-26537},
  doi =		{10.4230/LIPIcs.RTA.2010.193},
  annote =	{Keywords: Unification, sorts, regular expression}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact