Priv.-Doz. Dipl.-Math. Dr. Teimuraz Kutsia

Course Id	Title	Registration	Type	Hours	Teachers	Rhythm
326.0AR (2024W)	Automated Reasoning Further information	Register	VL	3,0	Teimuraz Kutsia Tudor Jebelean	Weekly
326.122 (2024W)	Special Topics Logic Programming Further information	Register	VL	2,0	Teimuraz Kutsia	Weekly
326.063 (2024W)	Symbolic Computation Project seminar Formal Methods and Automated Reasoning Further information	Register	SE	2,0	Wolfgang Schreiner Teimuraz Kutsia Wolfgang Windsteiger	Weekly

Content provided by KUSSS, Johannes Kepler University Linz | E-Mail

Software

PρLog (pronounced Pē-rō-log) is an experimental tool that extends logic programming with strategic conditional transformation rules, combining Prolog with ρLog calculus. It deals with term sequences (also called hedges), transforming them by conditional rules. Transformations are nondeterministic and may yield ...

Authors: Teimuraz Kutsia, Mircea Marin

More Software Website

Theorema

A Mathematical Assistant System implemented in Mathematica

The present prototype version of the Theorema software system is implemented in Mathematica . The system consists of a general higher-order predicate logic prover and a collection of special provers that call each other depending on the particular proof situations. ...

Authors: Alexander Maletzky, Bruno Buchberger, Markus Rosenkranz, Nikolaj Popov, Teimuraz Kutsia, Tudor Jebelean, Wolfgang Windsteiger

More Software Website

Unification and Anti-Unification Algorithm Library

This library contains unification, matching, and anti-unification algorithms in various theories developed at RISC. Unification with sequence variables. Context sequence matching. Rigid anti-unification for unranked terms and hedges and its experimental extension with commutative symbols. Unranked second-order anti-unification and its ...

Authors: Teimuraz Kutsia, Alexander Baumgartner, David Cerna

More Software Website

Publications

2024

[Kutsia]

Solving Quantitative Equations

G. Ehling, T. Kutsia

Technical report no. 24-03 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). April 2024. Licensed under CC BY 4.0 International. [doi] [pdf]

[bib]

@techreport{RISC7056,
author = {G. Ehling and T. Kutsia},
title = {{Solving Quantitative Equations}},
language = {english},
abstract = {Quantitative equational reasoning provides a framework that extends equality to an abstract notion of proximity by endowing equations with an element of a quantale. In this paper, we discuss the unification problem for a special class of shallow subterm-collapse-free quantitative equational theories. We outline rule-based algorithms for solving such equational unification problems over generic as well as idempotent Lawvereian quantales and study their properties.},
number = {24-03},
year = {2024},
month = {April},
keywords = {quantitative equational reasoning, Lawvereian quantales, equational unification},
length = {23},
license = {CC BY 4.0 International},
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]

Equational Anti-unification over Absorption Theories

Mauricio Ayala-Rincón, David M. Cerna, Andres Felipe Gonzalez Barragan, Temur Kutsia

In: Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Christoph Benzmüller, Marijn J. H. Heule, Renate A. Schmidt (ed.), Lecture Notes in Artificial Intelligence 14740, pp. 317-337. 2024. Springer, ISBN 978-3-031-63500-7. [doi]

[bib]

@inproceedings{RISC7064,
author = {Mauricio Ayala-Rincón and David M. Cerna and Andres Felipe Gonzalez Barragan and Temur Kutsia},
title = {{Equational Anti-unification over Absorption Theories}},
booktitle = {{Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings}},
language = {english},
series = {Lecture Notes in Artificial Intelligence},
volume = {14740},
pages = {317--337},
publisher = {Springer},
isbn_issn = {ISBN 978-3-031-63500-7},
year = {2024},
editor = {Christoph Benzmüller and Marijn J. H. Heule and Renate A. Schmidt},
refereed = {yes},
length = {21},
url = {https://doi.org/10.1007/978-3-031-63501-4_17}
}

[Kutsia]

Solving Quantitative Equations

Georg Ehling, Temur Kutsia

In: Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Christoph Benzmüller, Marijn J. H. Heule, Renate A. Schmidt (ed.), Lecture Notes in Artificial Intelligence 14740, pp. 381-400. 2024. Springer, ISBN 978-3-031-63500-7. [doi]

[bib]

@inproceedings{RISC7065,
author = {Georg Ehling and Temur Kutsia},
title = {{Solving Quantitative Equations}},
booktitle = {{Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings}},
language = {english},
series = {Lecture Notes in Artificial Intelligence},
volume = {14740},
pages = {381--400},
publisher = {Springer},
isbn_issn = {ISBN 978-3-031-63500-7},
year = {2024},
editor = {Christoph Benzmüller and Marijn J. H. Heule and Renate A. Schmidt},
refereed = {yes},
length = {20},
url = {https://doi.org/10.1007/978-3-031-63501-4_20}
}

2023

[Kutsia]

Anti-unification and Generalization: a Survey

David Cerna, Temur Kutsia

In: Proceedings of IJCAI 2023 - 32nd International Joint Conference on Artifical Intelligence, Edith Elkind (ed.), pp. 6563-6573. 2023. ijcai.org, ISBN 978-1-956792-03-4 . [doi]

[bib]

@inproceedings{RISC6743,
author = {David Cerna and Temur Kutsia},
title = {{Anti-unification and Generalization: a Survey}},
booktitle = {{Proceedings of IJCAI 2023 - 32nd International Joint Conference on Artifical Intelligence}},
language = {english},
pages = {6563--6573},
publisher = {ijcai.org},
isbn_issn = {ISBN 978-1-956792-03-4 },
year = {2023},
editor = {Edith Elkind},
refereed = {yes},
length = {11},
url = {https://doi.org/10.24963/ijcai.2023/736}
}

[Kutsia]

Nominal AC-Matching

Mauricio Ayala-Rincón, Maribel Fernández, Gabriel Ferreira Silva, Temur Kutsia, and Daniele Nantes-Sobrinho

In: Proceedings of the 16th International Conference on Intelligent Computer Mathematics, CICM 2023, Catherine Dubois and Manfred Kerber (ed.), Lecture Notes in Aritificial Intelligence 14101, pp. 53-68. 2023. Springer, ISBN 978-3-031-42752-7. [doi]

[bib]

@inproceedings{RISC6744,
author = {Mauricio Ayala-Rincón and Maribel Fernández and Gabriel Ferreira Silva and Temur Kutsia and and Daniele Nantes-Sobrinho},
title = {{Nominal AC-Matching}},
booktitle = {{Proceedings of the 16th International Conference on Intelligent Computer Mathematics, CICM 2023}},
language = {english},
series = {Lecture Notes in Aritificial Intelligence},
volume = {14101},
pages = {53--68},
publisher = {Springer},
isbn_issn = {ISBN 978-3-031-42752-7},
year = {2023},
editor = {Catherine Dubois and Manfred Kerber},
refereed = {yes},
length = {16},
url = {https://doi.org/10.1007/978-3-031-42753-4_4}
}

[Kutsia]

Enumerating All Maximal Clique-Partitions of an Undirected Graph

Mircea Marin, Temur Kutsia, Cleo Pau, Mikheil Rukhaia

In: Proceedings 7th Symposium on Working Formal Methods, FROM 2023, Horatiu Cheval, Laurentiu Leustean, and Andrei Sipos (ed.), pp. 65-79. 2023. [doi]

[bib]

@inproceedings{RISC6882,
author = {Mircea Marin and Temur Kutsia and Cleo Pau and Mikheil Rukhaia},
title = {{Enumerating All Maximal Clique-Partitions of an Undirected Graph}},
booktitle = {{Proceedings 7th Symposium on Working Formal Methods, FROM 2023}},
language = {english},
pages = {65--79},
isbn_issn = { },
year = {2023},
editor = {Horatiu Cheval and Laurentiu Leustean and and Andrei Sipos},
refereed = {yes},
length = {15},
url = {https://doi.org/10.4204/EPTCS.389.6}
}

[Kutsia]

Equational Anti-Unification over Absorption Theories

Mauricio Ayala-Rincón, David M. Cerna, Andres Felipe Gonzalez Barragan, Temur Kutsia

arXiv:2310.11136. Technical report, 2023. [doi]

[bib]

@techreport{RISC6884,
author = {Mauricio Ayala-Rincón and David M. Cerna and Andres Felipe Gonzalez Barragan and Temur Kutsia},
title = {{Equational Anti-Unification over Absorption Theories}},
language = {english},
year = {2023},
institution = {arXiv:2310.11136},
length = {23},
url = {https://doi.org/10.48550/arXiv.2310.11136}
}

[Kutsia]

Matching in Quantitative Equational Theories

Georg Ehling, Temur Kutsia

In: UNIF 2023 - 37th International Workshop on Unification, Veena Ravishankar and Christophe Ringeissen (ed.), pp. -. 2023. [url]

[bib]

@inproceedings{RISC6885,
author = {Georg Ehling and Temur Kutsia},
title = {{Matching in Quantitative Equational Theories}},
booktitle = {{UNIF 2023 - 37th International Workshop on Unification}},
language = {english},
pages = {--},
isbn_issn = { },
year = {2023},
editor = {Veena Ravishankar and Christophe Ringeissen},
refereed = {yes},
sponsor = {FWF},
length = {7},
url = {https://inria.hal.science/hal-04128216}
}

2022

[Kutsia]

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}
}

[Kutsia]

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]

A framework for approximate generalization in quantitative theories

Temur Kutsia, Cleo Pau

Technical report no. 22-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). May 2022. Licensed under CC BY 4.0 International. [doi] [pdf]

[bib]

@techreport{RISC6505,
author = {Temur Kutsia and Cleo Pau},
title = {{A framework for approximate generalization in quantitative theories}},
language = {english},
abstract = {Anti-unification aims at computing generalizations for given terms, retaining their common structure and abstracting differences by variables. We study quantitative anti-unification where the notion of the common structure is relaxed into "proximal'' up to the given degree with respect to the given fuzzy proximity relation. Proximal symbols may have different names and arities. We develop a generic set of rules for computing minimal complete sets of approximate generalizations and study their properties. Depending on the characterizations of proximities between symbols and the desired forms of solutions, these rules give rise to different versions of concrete algorithms.},
number = {22-04},
year = {2022},
month = {May},
keywords = {Generalization, anti-unification, quantiative theories, fuzzy proximity relations},
length = {22},
license = {CC BY 4.0 International},
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]

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}
}

[Kutsia]

A Framework for Approximate Generalization in Quantitative Theories

Temur Kutsia and Cleo Pau

In: Automated Reasoning, Jasmin Blanchette, Laura Kovács, and Dirk Pattinson (ed.), Proceedings of 11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022, Lecture Notes in Artificial Intelligence 13385, pp. 578-596. 2022. Springer, ISBN 978-3-031-10768-9. [doi]

[bib]

@inproceedings{RISC6631,
author = {Temur Kutsia and Cleo Pau},
title = {{A Framework for Approximate Generalization in Quantitative Theories}},
booktitle = {{Automated Reasoning}},
language = {english},
series = {Lecture Notes in Artificial Intelligence},
volume = {13385},
pages = {578--596},
publisher = {Springer},
isbn_issn = {ISBN 978-3-031-10768-9},
year = {2022},
editor = {Jasmin Blanchette and Laura Kovács and and Dirk Pattinson},
refereed = {yes},
sponsor = {FWF},
length = {19},
conferencename = {11th International Joint Conference, IJCAR 2022, Haifa, Israel, August 8-10, 2022},
url = {https://doi.org/10.1007/978-3-031-10769-6}
}

[Kutsia]

Work-in-progress papers presented at the 15th Conference on Intelligent Computer Mathematics, CICM 2022 (Informal Proceedings)

Kevin Buzzard and Temur Kutsia

, 2022. [url] [pdf]

[bib]

@techreport{RISC6584,
author = {Kevin Buzzard and Temur Kutsia},
title = {{Work-in-progress papers presented at the 15th Conference on Intelligent Computer Mathematics, CICM 2022 (Informal Proceedings)}},
language = {english},
year = {2022},
institution = { },
length = {77},
url = {https://cicm-conference.org/2022/cicm.php}
}

2021

[Kutsia]

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}
}

[Kutsia]

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)}
}

[Kutsia]

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)}
}

[Kutsia]

9th International Symposium on Symbolic Computation in Software Science (SCSS 2021), short and work-in-progress papers

Temur Kutsia (editor)

Technical report no. 21-16 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). August 2021. Licensed under CC BY 4.0 International. [doi] [pdf]

[bib]

@techreport{RISC6359,
author = {Temur Kutsia (editor)},
title = {{9th International Symposium on Symbolic Computation in Software Science (SCSS 2021), short and work-in-progress papers}},
language = {english},
abstract = {This collection contains short and work-in-progress papers presented at the 9th International Symposium on Symbolic Computation in Software Science, SCSS 2021.},
number = {21-16},
year = {2021},
month = {August},
keywords = {Symbolic computation, software science, artificial intelligence},
length = {56},
license = {CC BY 4.0 International},
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]

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

[Kutsia]

McCarthy-Kleene fuzzy automata and MSO logics

Manfred Droste, Temur Kutsia, George Rahonis, Wolfgang Schreiner

Information and Computation, pp. -. 2020. Elsevier, ISSN 0890-5401. In Press. [doi]

[bib]

@article{RISC6011,
author = {Manfred Droste and Temur Kutsia and George Rahonis and Wolfgang Schreiner},
title = {{McCarthy-Kleene fuzzy automata and MSO logics}},
language = {english},
abstract = {We introduce McCarthy-Kleene fuzzy automata (MK-fuzzy automata) over a bimonoid K which is related to the fuzzification of the McCarthy-Kleene logic. Our automata are inspired by, and intend to contribute to, practical applications being in development in a project on runtime network monitoring based on predicate logic. We investigate closure properties of the class of recognizable MK-fuzzy languages accepted by MK-fuzzy automata as well as of deterministically recognizable MK-fuzzy languages accepted by their deterministic counterparts. Moreover, we establish a Nivat-like result for recognizable MK-fuzzy languages. We introduce an MK-fuzzy MSO logic and show the expressive equivalence of a fragment of this logic with MK-fuzzy automata, i.e., a Büchi type theorem.},
journal = {Information and Computation},
pages = {--},
publisher = {Elsevier},
isbn_issn = {ISSN 0890-5401},
year = {2020},
note = {In Press},
refereed = {yes},
keywords = {Bimonoids, McCarthy-Kleene logic, MK-fuzzy automata, MK-fuzzy MSO logic},
sponsor = {Supported by the Austrian Research Promotion Agency (FFG) in the frame of the BRIDGE program 846003 “LogicGuard II”},
length = {23},
url = {https://doi.org/10.1016/j.ic.2019.104499}
}