Rewriting-related Techniques and Applications

We investigate solving methods for equational and membership constraints, generalization techniques in various theories, and calculi for conditional rule-based transformations. The developed algorithms and procedures are useful for equational reasoning, program analysis, and declarative programming. Our research interests also include rewriting-based deduction, models of computation, and computer security.

Rewriting has been playing an important role in symbolic computation and automated deduction. We are interested in fundamental algorithmic problems for rewriting-based techniques as well as in applications of rewriting-related frameworks in programming and reasoning.

Unification and matching are fundamental computational techniques for automated reasoning, term rewriting, and declarative programming. Essentially, they can be seen as methods for solving equations between terms. The difficulty of an unification problem depends on many parameters, e.g., the background equational theory, the order of the language, the presence of sorts, the representation of objects, etc. We have been investigating this problem under various combinations of those parameters, developing solving procedures, proving their properties, providing prototype implementations, identifying well-behaved special cases, and studying practical applications. Some of those algorithms have been included in the mathematical assistant system Theorema and in the rule-based programming tool PρLog. See also the Web page of the SToUT project.

Anti-unification is yet another fundamental technique originating from inductive reasoning. Its goal is to find an object which generalizes the given objects: retaining similarities between them as much as possible, and abstracting over the differences by variables. Unification and anti-unification are considered as dual methods in the following sense: solutions of an unification problem give most general common instance of the given expressions, while anti-unification computes their least general common generalization. We are interested in designing new anti-unification algorithms for various first- and higher-order theories, proving their properties, investigating complexity, providing implementations, and applying them in software code clone detection, program synthesis, and natural language processing. We have been developing an open-source online library of unification and anti-unification algorithms. See also the Web page of the GALA project.

We have contributed in the development of a calculus for conditional sequence transformations by strategies, called ρLog, which forms the theoretical basis of the rule-based programming tool PρLog. It deals with term sequences (also called hedges), transforming them by conditional rules. Transformations are nondeterministic and may yield several results. Strategies provide a control on rule applications in a declarative way. The transformation rules are combined with logic programming. See more details on the PρLog Web page.

Our other interests include equational reasoning, pattern calculi, and runtime verification. See the publication list below for relevant references.

Members

Loading…

Ongoing Projects

Software

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
MoreSoftware Website

Publications

2024

[AUTHOR]

Proximity-based matching with arbitrary T-norms

Maximilian Donnermair

RISC, Johannes Kepler University Linz. Bachelor Thesis. 2024. [pdf]
[bib]
@misc{RISC7061,
author = {Maximilian Donnermair},
title = {{Proximity-based matching with arbitrary T-norms}},
language = {english},
year = {2024},
translation = {0},
institution = {RISC, Johannes Kepler University Linz},
length = {38}
}
[Cerna]

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}
}
[Ehling]

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)}
}
[Ehling]

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

[Buchberger]

Automated Programming, Symbolic computation, Machine Learning: My Personal View

Bruno Buchberger

Ann. Math. Artif. Intell. 91(5), pp. 569-589. 2023. 1012-2443.
[bib]
@article{RISC6895,
author = {Bruno Buchberger},
title = {{Automated Programming, Symbolic computation, Machine Learning: My Personal View}},
language = {english},
journal = {Ann. Math. Artif. Intell.},
volume = {91},
number = {5},
pages = {569--589},
isbn_issn = {1012-2443},
year = {2023},
refereed = {yes},
length = {21}
}
[Buchberger]

International Young Talents Hotspot Austria

Bruno Buchberger

In: Ideen, die gehen!, W. Schüssel, G. Kneifel (ed.), pp. 37-39. 2023. Edition Kleine Zeitung, 20234.
[bib]
@incollection{RISC6896,
author = {Bruno Buchberger},
title = {{International Young Talents Hotspot Austria}},
booktitle = {{Ideen, die gehen!}},
language = {english},
pages = {37--39},
publisher = {Edition Kleine Zeitung},
isbn_issn = {20234},
year = {2023},
editor = {W. Schüssel and G. Kneifel},
refereed = {no},
length = {3}
}
[Buchberger]

Wissenschaft und Meditation: Auf dem Weg zur bewussten Naturgesellschaft

Bruno Buchberger

1st edition, December 2023. Amazon, 979-8868299117.
[bib]
@book{RISC6898,
author = {Bruno Buchberger},
title = {{Wissenschaft und Meditation: Auf dem Weg zur bewussten Naturgesellschaft}},
language = {german},
publisher = {Amazon},
isbn_issn = {979-8868299117},
year = {2023},
month = {December},
edition = {1st},
translation = {0},
length = {184}
}
[Cerna]

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}
}
[Cerna]

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}
}
[Ehling]

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}
}
[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}
}
[Pau]

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

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

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)}
}
[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}
}
[Pau]

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

2021

[Cerna]

A Special Case of Schematic Syntactic Unification

David M. Cerna

CAS ICS / RISC. Technical report, 2021. [pdf]
[bib]
@techreport{RISC6349,
author = {David M. Cerna},
title = {{A Special Case of Schematic Syntactic Unification}},
language = {english},
abstract = {We present a unification problem based on first-order syntactic unification which ask whether every problemin a schematically-defined sequence of unification problems isunifiable, so called loop unification. Alternatively, our problemmay be formulated as a recursive procedure calling first-ordersyntactic unification on certain bindings occurring in the solvedform resulting from unification. Loop unification is closely relatedto Narrowing as the schematic constructions can be seen as arewrite rule applied during unification, and primal grammars, aswe deal with recursive term constructions. However, loop unifi-cation relaxes the restrictions put on variables as fresh as wellas used extra variables may be introduced by rewriting. In thiswork we consider an important special case, so called semiloopunification. We provide a sufficient condition for unifiability of theentire sequence based on the structure of a sufficiently long initialsegment. It remains an open question whether this conditionis also necessary for semiloop unification and how it may beextended to loop unification.},
year = {2021},
institution = {CAS ICS / RISC},
length = {8}
}

Loading…