Generalization ALgorithms and Applications [GALA]

Project Lead

Project Duration

01/02/2016 - 31/01/2021

Project URL

Go to Website

Publications

2022

[Dundua]

Unranked Nominal Unification

Besik Dundua, Temur Kutsia, Mikheil Rukhaia

In: Proceedings of TbiLLC 2019 - 13th International Tbilisi Symposium on Logic, Language, and Computation, Aybüke Özgün and Yulia Zinova (ed.), Proceedings of 13th International Tbilisi Symposium on Logic, Language, and Computation, Lecture Notes in Computer Science 13206, pp. 279-296. 2022. Springer, ISBN 978-3-030-98478-6. [doi] [pdf]
[bib]
@inproceedings{RISC6498,
author = {Besik Dundua and Temur Kutsia and Mikheil Rukhaia},
title = {{Unranked Nominal Unification}},
booktitle = {{Proceedings of TbiLLC 2019 - 13th International Tbilisi Symposium on Logic, Language, and Computation}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {13206},
pages = {279--296},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-98478-6},
year = {2022},
editor = {Aybüke Özgün and Yulia Zinova},
refereed = {yes},
length = {17},
conferencename = {13th International Tbilisi Symposium on Logic, Language, and Computation},
url = {https://doi.org/10.1007/978-3-030-98479-3_14}
}
[Kutsia]

Nominal Unification and Matching of Higher Order Expressions with Recursive Let

Manfred Schmidt-Schauß, Temur Kutsia, Jordi Levy, Mateu Villaret, Yunus Kutz

Fundamenta Informaticae 185(3), pp. 247-283. 2022. IOS Press, ISSN 1875-8681. [url]
[bib]
@article{RISC6506,
author = {Manfred Schmidt-Schauß and Temur Kutsia and Jordi Levy and Mateu Villaret and Yunus Kutz},
title = {{Nominal Unification and Matching of Higher Order Expressions with Recursive Let}},
language = {english},
journal = {Fundamenta Informaticae},
volume = {185},
number = {3},
pages = {247--283},
publisher = {IOS Press},
isbn_issn = {ISSN 1875-8681},
year = {2022},
refereed = {yes},
length = {37},
url = {https://arxiv.org/abs/2102.08146v4}
}
[Pau]

Matching and Generalization Modulo Proximity and Tolerance Relations

Temur Kutsia, Cleo Pau

In: Proceedings of TbiLLC 2019 - 13th International Tbilisi Symposium on Logic, Language, and Computation, Aybüke Özgün and Yulia Zinova (ed.), Lecture Notes in Computer Science 13206, pp. 323-342. 2022. Springer, ISBN 978-3-030-98478-6. [doi] [pdf]
[bib]
@inproceedings{RISC6491,
author = {Temur Kutsia and Cleo Pau},
title = {{Matching and Generalization Modulo Proximity and Tolerance Relations}},
booktitle = {{Proceedings of TbiLLC 2019 - 13th International Tbilisi Symposium on Logic, Language, and Computation}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {13206},
pages = {323--342},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-98478-6},
year = {2022},
editor = {Aybüke Özgün and Yulia Zinova},
refereed = {yes},
length = {20},
url = {https://doi.org/10.1007/978-3-030-98479-3_16}
}
[Pau]

Symbolic Techniques for Approximate Reasoning

Cleo Pau

RISC, JKU. PhD Thesis. 2022. [pdf]
[bib]
@phdthesis{RISC6513,
author = {Cleo Pau},
title = {{Symbolic Techniques for Approximate Reasoning}},
language = {english},
year = {2022},
translation = {0},
school = {RISC, JKU},
length = {202}
}

2021

[Dundua]

Variadic equational matching in associative and commutative theories

Besik Dundua, Temur Kutsia, Mircea Marin

Journal of Symbolic Computation 106, pp. 78-109. 2021. Elsevier, ISSN 0747-7171. [doi] [pdf]
[bib]
@article{RISC6260,
author = {Besik Dundua and Temur Kutsia and Mircea Marin},
title = {{Variadic equational matching in associative and commutative theories}},
language = {english},
journal = {Journal of Symbolic Computation},
volume = {106},
pages = {78--109},
publisher = {Elsevier},
isbn_issn = {ISSN 0747-7171},
year = {2021},
refereed = {yes},
length = {32},
url = {https://doi.org/10.1016/j.jsc.2021.01.001}
}
[Pau]

Proximity-Based Unification and Matching for Full Fuzzy Signatures

Temur Kutsia, Cleo Pau

Technical report no. 21-08 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). April 2021. [doi] [pdf]
[bib]
@techreport{RISC6296,
author = {Temur Kutsia and Cleo Pau},
title = {{Proximity-Based Unification and Matching for Full Fuzzy Signatures}},
language = {english},
abstract = {Proximity relations are binary fuzzy relations, which are reflexiveand symmetric, but not transitive. We propose proximity-based unification and matching algorithms in fuzzy languages whose signaturestolerate mismatches in function symbol names, arity, and in the arguments order (so called full fuzzy signatures). This work generalizeson the one hand, proximity-based unification to full fuzzy signatures,and on the other hand, similarity-based unification over a full fuzzysignature by extending similarity to proximity.},
number = {21-08},
year = {2021},
month = {April},
keywords = {Fuzzy proximity relations, Unification Matching, Arity mismatch},
length = {15},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Pau]

Generalization Algorithms with Proximity Relations in Full Fuzzy Signatures

Temur Kutsia, Cleo Pau

Technical report no. 21-09 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). April 2021. [doi] [pdf]
[bib]
@techreport{RISC6297,
author = {Temur Kutsia and Cleo Pau},
title = {{Generalization Algorithms with Proximity Relations in Full Fuzzy Signatures}},
language = {english},
abstract = {Anti-unification aims at computing generalizations for given terms,retaining their common structure and abstracting differences by variables. We study anti-unification for full fuzzy signatures, where thenotion of common structure is relaxed into a ``proximal'' one with re-spect to a given proximity relation. Mismatches between both symbolnames and their arities are permitted. We develop algorithms for different cases of the problem and study their properties.},
number = {21-09},
year = {2021},
month = {April},
keywords = {Fuzzy proximity relations, Generalization, Anti-unification, Arity mismatch},
length = {15},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Pau]

Proximity-Based Unification and Matching for Fully Fuzzy Signatures

Cleo Pau, Temur Kutsia

In: Proceedings of the 30th IEEE International Conference on Fuzzy Systems, FUZZ-IEEE 2021, , pp. 1-6. 2021. IEEE, isbn 978-1-6654-4407-1. [doi] [pdf]
[bib]
@inproceedings{RISC6369,
author = {Cleo Pau and Temur Kutsia},
title = {{Proximity-Based Unification and Matching for Fully Fuzzy Signatures}},
booktitle = {{Proceedings of the 30th IEEE International Conference on Fuzzy Systems, FUZZ-IEEE 2021}},
language = {english},
pages = {1--6},
publisher = {IEEE},
isbn_issn = {isbn 978-1-6654-4407-1},
year = {2021},
editor = { },
refereed = {yes},
length = {6},
url = {https://doi.org/10.1109/FUZZ45933.2021.9494438}
}

2020

[Cerna]

Idempotent Anti-unification

David Cerna, Temur Kutsia

ACM Transactions on Computational Logic (TOCL) 21(2), pp. 10:1-10:32. 2020. ACM Press, ISSN 1529-3785. [doi] [pdf]
[bib]
@article{RISC6023,
author = {David Cerna and Temur Kutsia},
title = {{Idempotent Anti-unification}},
language = {english},
journal = {ACM Transactions on Computational Logic (TOCL)},
volume = {21},
number = {2},
pages = {10:1--10:32},
publisher = {ACM Press},
isbn_issn = {ISSN 1529-3785},
year = {2020},
refereed = {yes},
length = {32},
url = {https://doi.org/10.1145/3359060}
}
[Cerna]

Unital Anti-Unification: Type and Algorithms

David M. Cerna , Temur Kutsia

In: 5th International Conference on Formal Structures for Computation and Deduction, {FSCD} 2020, June 29-July 6, 2020, Paris, France (Virtual Conference, Zena M. Ariola (ed.), Proceedings of FSCD, LIPICS 167/20-02, pp. 1-20. 2020. 1868-8969. [doi]
[bib]
@inproceedings{RISC6237,
author = {David M. Cerna and Temur Kutsia},
title = {{Unital Anti-Unification: Type and Algorithms}},
booktitle = {{5th International Conference on Formal Structures for Computation and Deduction, {FSCD} 2020, June 29-July 6, 2020, Paris, France (Virtual Conference}},
language = {english},
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 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. },
series = {LIPICS},
volume = {167},
number = {20-02},
pages = {1--20},
isbn_issn = {1868-8969},
year = {2020},
editor = {Zena M. Ariola},
refereed = {yes},
keywords = {Anti-unification, tree grammars, unital theories, collapse theories},
length = {19},
conferencename = {FSCD},
url = {https://doi.org/10.4230/LIPIcs.FSCD.2020.26}
}
[Dundua]

Constraint Solving over Multiple Similarity Relations

Besik Dundua, Temur Kutsia, Mircea Marin, Cleopatra Pau

In: Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020), Zena M. Ariola (ed.), Leibniz International Proceedings in Informatics (LIPIcs) 167, pp. 30:1-30:19. 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, ISBN 978-3-95977-155-9, ISSN 1868-8969. [doi]
[bib]
@inproceedings{RISC6133,
author = {Besik Dundua and Temur Kutsia and Mircea Marin and Cleopatra Pau},
title = {{Constraint Solving over Multiple Similarity Relations}},
booktitle = {{Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {167},
pages = {30:1--30:19},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
isbn_issn = {ISBN 978-3-95977-155-9, ISSN 1868-8969},
year = {2020},
editor = {Zena M. Ariola},
refereed = {yes},
length = {19},
url = {https://doi.org/10.4230/LIPIcs.FSCD.2020.30}
}
[Dundua]

Specification and Analysis of ABAC Policies in a Rule-Based Framework

Besik Dundua, Temur Kutsia, Mircea Marin, Mikheil Rukhaia

In: AMINSE 2019: Applications of Mathematics and Informatics in Natural Sciences and Engineering, George Jaiani, David Natroshvili (ed.), Springer Proceedings in Mathematics & Statistics 334, pp. 101-116. 2020. Springer, ISBN 978-3-030-56356-1, 978-3-030-56355-4. [doi] [pdf]
[bib]
@incollection{RISC6228,
author = {Besik Dundua and Temur Kutsia and Mircea Marin and Mikheil Rukhaia},
title = {{Specification and Analysis of ABAC Policies in a Rule-Based Framework}},
booktitle = {{AMINSE 2019: Applications of Mathematics and Informatics in Natural Sciences and Engineering}},
language = {english},
series = {Springer Proceedings in Mathematics & Statistics},
volume = {334},
pages = {101--116},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-56356-1, 978-3-030-56355-4},
year = {2020},
editor = {George Jaiani and David Natroshvili},
refereed = {yes},
length = {16},
url = {https://doi.org/10.1007/978-3-030-56356-1_7}
}
[Dundua]

A Rule-Based System for Computation and Deduction in Mathematica

Mircea Marin, Besik Dundua, Temur Kutsia

In: WRLA 2020: Rewriting Logic and Its Applications, Santiago Escobar, Narciso Martí-Oliet (ed.), Lecture Notes in Computer Science 12328, pp. 57-74. 2020. Springer, ISBN 978-3-030-63595-4, 978-3-030-63594-7. [doi] [pdf]
[bib]
@inproceedings{RISC6229,
author = {Mircea Marin and Besik Dundua and Temur Kutsia},
title = {{A Rule-Based System for Computation and Deduction in Mathematica}},
booktitle = {{WRLA 2020: Rewriting Logic and Its Applications}},
language = {english},
series = { Lecture Notes in Computer Science},
volume = {12328},
pages = {57--74},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-63595-4, 978-3-030-63594-7},
year = {2020},
editor = {Santiago Escobar and Narciso Martí-Oliet},
refereed = {yes},
length = {18},
url = {https://doi.org/10.1007/978-3-030-63595-4_4}
}
[Dundua]

Extending the 𝜌Log Calculus with Proximity Relations

Besik Dundua, Temur Kutsia, Mircea Marin, Cleo Pau

In: AMINSE 2019: Applications of Mathematics and Informatics in Natural Sciences and Engineering, George Jaiani, David Natroshvili (ed.), Springer Proceedings in Mathematics & Statistics 334, pp. 83-100. 2020. Springer, ISBN 978-3-030-56356-1, 978-3-030-56355-4. [doi] [pdf]
[bib]
@incollection{RISC6227,
author = {Besik Dundua and Temur Kutsia and Mircea Marin and Cleo Pau},
title = {{Extending the 𝜌Log Calculus with Proximity Relations}},
booktitle = {{AMINSE 2019: Applications of Mathematics and Informatics in Natural Sciences and Engineering}},
language = {english},
series = {Springer Proceedings in Mathematics & Statistics},
volume = {334},
pages = {83--100},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-56356-1, 978-3-030-56355-4},
year = {2020},
editor = {George Jaiani and David Natroshvili},
refereed = {yes},
length = {18},
url = {https://doi.org/10.1007/978-3-030-56356-1_6}
}
[Dundua]

Unranked Nominal Unification

Besik Dundua, Temur Kutsia, Mikheil Rukhaia

Technical report no. 20-21 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). 2020. [pdf]
[bib]
@techreport{RISC6273,
author = {Besik Dundua and Temur Kutsia and Mikheil Rukhaia},
title = {{Unranked Nominal Unification}},
language = {english},
number = {20-21},
year = {2020},
sponsor = {FWF, project 28789-N32},
length = {18},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Kutsia]

Proceedings of The 34th International Workshop on Unification, UNIF 2020

Temur Kutsia and Andrew M. Marshall (Editors)

Technical report no. 20-10 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). 2020. [pdf]
[bib]
@techreport{RISC6129,
author = {Temur Kutsia and Andrew M. Marshall (Editors)},
title = {{Proceedings of The 34th International Workshop on Unification, UNIF 2020}},
language = {english},
number = {20-10},
year = {2020},
length = {82},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Kutsia]

Unification modulo alpha-equivalence in a mathematical assistant system

Temur Kutsia

Technical report no. 20-01 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). 2020. [pdf]
[bib]
@techreport{RISC6074,
author = {Temur Kutsia},
title = {{Unification modulo alpha-equivalence in a mathematical assistant system}},
language = {english},
number = {20-01},
year = {2020},
length = {21},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Kutsia]

Constructing orthogonal designs in powers of two via symbolic computation and rewriting techniques

Ilias Kotsireas, Temur Kutsia, Dimitris Simos

Annals of Mathematics and Artificial Intelligence 88(1), pp. 213-236. 2020. ISSN 1573-7470. [doi] [pdf]
[bib]
@article{RISC6116,
author = {Ilias Kotsireas and Temur Kutsia and Dimitris Simos},
title = {{ Constructing orthogonal designs in powers of two via symbolic computation and rewriting techniques}},
language = {english},
journal = {Annals of Mathematics and Artificial Intelligence},
volume = {88},
number = {1},
pages = {213--236},
isbn_issn = {ISSN 1573-7470},
year = {2020},
refereed = {yes},
length = {24},
url = {https://doi.org/10.1007/s10472-018-9607-9}
}
[Pau]

Proximity-based Unification with Arity Mismatch

Temur Kutsia, Cleo Pau

In: Proceedings of the 34th International Workshop on Unification, Temur Kutsia, Andrew M. Marshall (ed.), pp. 9:1-9:6. 2020.
[bib]
@inproceedings{RISC6295,
author = {Temur Kutsia and Cleo Pau},
title = {{Proximity-based Unification with Arity Mismatch}},
booktitle = {{Proceedings of the 34th International Workshop on Unification}},
language = {english},
pages = {9:1--9:6},
isbn_issn = { },
year = {2020},
editor = {Temur Kutsia and Andrew M. Marshall},
refereed = {yes},
length = {6}
}

2019

[Cerna]

Higher-Order Pattern Generalization Modulo Equational Theories

David M. Cerna and Temur Kutsia

Submitted to the RISC Report Series. 2019. [pdf]
[bib]
@techreport{RISC5918,
author = {David M. Cerna and Temur Kutsia},
title = {{Higher-Order Pattern Generalization Modulo Equational Theories}},
language = {english},
abstract = {We consider anti-unification for simply typed lambda terms in theories defined by associativity, commutativity, identity (unit element) axioms and their combinations, and develop a sound and complete algorithm which takes two lambda terms and computes their equational generalizations in the form of higher-order patterns. The problem is finitary: the minimal complete set of such generalizations contains finitely many elements. We define the notion of optimal solution and investigate special restrictions of the problem for which the optimal solution can be computed in linear or polynomial time.The algorithm does not depend on the number of idempotent function symbols in the input terms. Thelanguage generated by the grammar is the minimal complete set of generalizations of the givenanti-unification problem, which implies that idempotent anti-unification is infinitary.},
year = {2019},
keywords = {Anti-unification Lambda Calculus},
length = {40},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}

Loading…