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

2026

[Dundua]

Quantitative Equational Rewriting

Besik Dundua, Georg Ehling, Santiago Escobar, Maribel Fernández, Temur Kutsia

Research Institute for Symbolic Computation, Johannes Kepler University Linz, Austria. Technical report, 2026. [pdf]
[bib]
@techreport{RISC7235,
author = {Besik Dundua and Georg Ehling and Santiago Escobar and Maribel Fernández and Temur Kutsia},
title = {{Quantitative Equational Rewriting}},
language = {english},
year = {2026},
institution = {Research Institute for Symbolic Computation, Johannes Kepler University Linz, Austria},
length = {35}
}

2025

[Baumgartner]

Equational Generalization Problems with Atom-Variables

Alexander Baumgartner, Temur Kutsia, Daniele Nantes-Sobrinho, Manfred Schmidt-Schauss

In: Intelligent Computer Mathematics - 18th International Conference, CICM 2025, Brasilia, Brazil, October 6-10, 2025, Proceedings, Valeria de Paiva and Peter Koepke (ed.), Lecture Notes in Computer Science 16136, pp. 133-151. 2025. Springer, ISBN 978-3-032-07020-3. [doi]
[bib]
@inproceedings{RISC7188,
author = {Alexander Baumgartner and Temur Kutsia and Daniele Nantes-Sobrinho and Manfred Schmidt-Schauss},
title = {{Equational Generalization Problems with Atom-Variables}},
booktitle = {{Intelligent Computer Mathematics - 18th International Conference, CICM 2025, Brasilia, Brazil, October 6-10, 2025, Proceedings}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {16136},
pages = {133--151},
publisher = {Springer},
isbn_issn = {ISBN 978-3-032-07020-3},
year = {2025},
editor = {Valeria de Paiva and Peter Koepke},
refereed = {yes},
length = {19},
url = {https://doi.org/10.1007/978-3-032-07021-0_8}
}
[Baumgartner]

Quantitative generalization of variadic structures with binders

Alexander Baumgartner, Temur Kutsia

Research Institute for Symbolic Computation, Johannes Kepler University Linz, Austria. Technical report, 2025. [pdf]
[bib]
@techreport{RISC7231,
author = {Alexander Baumgartner and Temur Kutsia},
title = {{Quantitative generalization of variadic structures with binders}},
language = {english},
year = {2025},
institution = {Research Institute for Symbolic Computation, Johannes Kepler University Linz, Austria},
length = {25}
}
[Cerna]

Combining Generalization Algorithms in Regular Collapse-Free Theories

Mauricio Ayala-Rincón, David Cerna, Temur Kutsia, Christophe Ringeissen

In: Proceedings of the 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025), Maribel Fernandez (ed.), LIPIcs - Leibniz International Proceedings in Informatics 337, pp. 7:1-7:18. 2025. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, ISBN 978-3-95977-374-4. [doi]
[bib]
@inproceedings{RISC7156,
author = {Mauricio Ayala-Rincón and David Cerna and Temur Kutsia and Christophe Ringeissen},
title = {{Combining Generalization Algorithms in Regular Collapse-Free Theories}},
booktitle = {{Proceedings of the 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025)}},
language = {english},
series = {LIPIcs - Leibniz International Proceedings in Informatics},
volume = {337},
pages = {7:1--7:18},
publisher = {Schloss Dagstuhl - Leibniz-Zentrum für Informatik},
isbn_issn = {ISBN 978-3-95977-374-4},
year = {2025},
editor = {Maribel Fernandez},
refereed = {yes},
length = {0},
url = {https://doi.org/10.4230/LIPIcs.FSCD.2025.7}
}
[Dundua]

Higher-Order Pattern Unification Modulo Similarity Relations

Besik Dundua, Temur Kutsia

Technical report no. 25-03 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). February 2025. Licensed under CC BY 4.0 International. [doi] [pdf]
[bib]
@techreport{RISC7141,
author = {Besik Dundua and Temur Kutsia},
title = {{Higher-Order Pattern Unification Modulo Similarity Relations}},
language = {english},
abstract = {The combination of higher-order theories and fuzzy logic can be useful in decision-making tasks that involve reasoning across abstract functions and predicates, where exact matches are often rare or unnecessary. Developing efficient reasoning and computational techniques for such a combined formalism presents a significant challenge. In this paper, we adopt a more straightforward approach aiming at integrating two well-established and computationally well-behaving components: higher-order patterns on one side and fuzzy equivalences expressed through similarity relations based on minimum T-norm on the other. We propose a unification algorithm for higher-order patterns modulo these similarity relations and prove its termination, soundness, and completeness. This unification problem, like its crisp counterpart, is unitary. The algorithm computes the most general unifier with the highest degree of approximation when the given terms are unifiable.},
number = {25-03},
year = {2025},
month = {February},
keywords = {Unification, higher-order patterns, fuzzy similarity relations},
length = {20},
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)}
}
[Dundua]

Higher-Order Pattern Unification Modulo Similarity Relations

Besik Dundua, Temur Kutsia

In: Proceedings of the 35th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2025, Santiago Escobar and Laura Titolo (ed.), Lecture Notes in Computer Science 16117, pp. 75-93. 2025. Springer, ISBN 978-3-032-04847-9. [doi] [pdf]
[bib]
@inproceedings{RISC7162,
author = {Besik Dundua and Temur Kutsia},
title = {{Higher-Order Pattern Unification Modulo Similarity Relations}},
booktitle = {{Proceedings of the 35th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR 2025}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {16117},
pages = {75--93},
publisher = {Springer},
isbn_issn = {ISBN 978-3-032-04847-9},
year = {2025},
editor = {Santiago Escobar and Laura Titolo},
refereed = {yes},
length = {19},
url = {https://doi.org/10.1007/978-3-032-04848-6_5}
}
[Ehling]

Graded Quantitative Narrowing

Mauricio Ayala-Rincon, Thaynara Arielly de Lima, Georg Ehling, Temur Kutsia

In: Intelligent Computer Mathematics - 18th International Conference, CICM 2025, Brasilia, Brazil, October 6-10, 2025, Proceedings, Valeria de Paiva and Peter Koepke (ed.), Lecture Notes in Computer Science 16136, pp. 113-132. 2025. Springer, ISBN 978-3-032-07020-3. [doi]
[bib]
@inproceedings{RISC7189,
author = {Mauricio Ayala-Rincon and Thaynara Arielly de Lima and Georg Ehling and Temur Kutsia},
title = {{Graded Quantitative Narrowing}},
booktitle = {{Intelligent Computer Mathematics - 18th International Conference, CICM 2025, Brasilia, Brazil, October 6-10, 2025, Proceedings}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {16136},
pages = {113--132},
publisher = {Springer},
isbn_issn = {ISBN 978-3-032-07020-3},
year = {2025},
editor = {Valeria de Paiva and Peter Koepke},
refereed = {yes},
length = {20},
url = {https://doi.org/10.1007/978-3-032-07021-0_7}
}
[Kutsia]

Verification of an Anti-unification Algorithm in PVS

Mauricio Ayala-Rincón, Thaynara Arielly de Lima, Maria Júlia Dias Lima, Mariano Miguel Moscato, and Temur Kutsia

In: NASA Formal Methods, Aaron Dutle, Laura Humphrey, Laura Titolo (ed.), Proceedings of The 17th NASA Formal Methods Symposium, NFM 2025, Williamsburg, VA, USA, Lecture Notes in Computer Science 15682, pp. 54-71. 2025. Springer, ISBN 978-3-031-93705-7. [doi]
[bib]
@inproceedings{RISC7152,
author = {Mauricio Ayala-Rincón and Thaynara Arielly de Lima and Maria Júlia Dias Lima and Mariano Miguel Moscato and and Temur Kutsia},
title = {{Verification of an Anti-unification Algorithm in PVS}},
booktitle = {{NASA Formal Methods}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {15682},
pages = {54--71},
publisher = {Springer},
isbn_issn = {ISBN 978-3-031-93705-7},
year = {2025},
editor = {Aaron Dutle and Laura Humphrey and Laura Titolo},
refereed = {yes},
length = {18},
conferencename = {The 17th NASA Formal Methods Symposium, NFM 2025, Williamsburg, VA, USA},
url = {https://doi.org/10.1007/978-3-031-93706-4_4}
}
[Sunthimer]

An Implementation of Approximate Generalization in Quantitative Theories

Daniel D. Sunthimer

Research Institute for Symbolic Computation, Johannes Kepler University Linz, Austria. Bachelor Thesis. 2025. [pdf]
[bib]
@misc{RISC7159,
author = {Daniel D. Sunthimer},
title = {{An Implementation of Approximate Generalization in Quantitative Theories}},
language = {english},
year = {2025},
translation = {0},
institution = {Research Institute for Symbolic Computation, Johannes Kepler University Linz, Austria},
length = {27}
}

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

Science and Meditation: Creating the Future (English Translation of "Wissenschaft und Meditation")

Bruno Buchberger

1st edition, 2024. Amazon, ‎ 979-8332230837.
[bib]
@book{RISC7102,
author = {Bruno Buchberger},
title = {{Science and Meditation: Creating the Future (English Translation of "Wissenschaft und Meditation")}},
language = {english},
publisher = {Amazon},
isbn_issn = { ‎ 979-8332230837},
year = {2024},
edition = {1st},
translation = {0},
length = {153}
}
[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}
}
[Dramnesc]

Certification of Tail Recursive Bubble-Sort in Theorema and Coq

I. Dramnesc, T. Jebelean, S. Stratulat

In: LPAR 2024 Complementary Volume, N. Bjørner, M. Heule, A. Voronkov (ed.), Kalpa Publications in Computing 18, pp. 53-68. 2024. EasyChair, ISSN 2515-1762. [url]
[bib]
@inproceedings{RISC7125,
author = {I. Dramnesc and T. Jebelean and S. Stratulat},
title = {{Certification of Tail Recursive Bubble-Sort in Theorema and Coq}},
booktitle = {{LPAR 2024 Complementary Volume}},
language = {English},
series = {Kalpa Publications in Computing},
volume = {18},
pages = {53--68},
publisher = {EasyChair},
isbn_issn = { ISSN 2515-1762},
year = {2024},
editor = {N. Bjørner and M. Heule and A. Voronkov},
refereed = {yes},
length = {16},
url = {/publications/paper/tbwq}
}
[Dramnesc]

Certification of Sorting Algorithms Using Theorema and Coq

I. Dramnesc, T. Jebelean, S. Stratulat

In: SCSS 2024, Symbolic Computation in Software Science , S. M. Watt, T. Ida (ed.), Lecture Notes in Artificial Intelligence 14991, pp. 38-56. 2024. Springer, ISBN 978-3-031-69041-9.
[bib]
@inproceedings{RISC7127,
author = {I. Dramnesc and T. Jebelean and S. Stratulat},
title = {{Certification of Sorting Algorithms Using Theorema and Coq}},
booktitle = {{SCSS 2024, Symbolic Computation in Software Science }},
language = {English},
series = {Lecture Notes in Artificial Intelligence},
volume = {14991},
pages = {38--56},
publisher = {Springer},
isbn_issn = {ISBN 978-3-031-69041-9},
year = {2024},
editor = {S. M. Watt and T. Ida},
refereed = {yes},
length = {19}
}
[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}
}
[Kutsia]

Certified First-Order AC-Unification and Applications

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

Journal of Automated Reasoning 68(4), pp. 25:1-25:48. 2024. ISSN 0168-7433. [doi] [pdf]
[bib]
@article{RISC7111,
author = {Mauricio Ayala-Rincón and Maribel Fernández and Gabriel Ferreira Silva and Temur Kutsia and Daniele Nantes-Sobrinho},
title = {{Certified First-Order AC-Unification and Applications}},
language = {english},
journal = {Journal of Automated Reasoning},
volume = {68},
number = {4},
pages = {25:1--25:48},
isbn_issn = {ISSN 0168-7433},
year = {2024},
refereed = {yes},
length = {0},
url = {https://doi.org/10.1007/s10817-024-09714-5}
}

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

Loading…