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

2020

[Cerna]

Unital Anti-Unification: Type and Algorithms

David M. Cerna , Temur Kutsia

Technical report no. 20-02 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. RISC Report, Febrary 2020. [pdf]
[bib]
@techreport{RISC6080,
author = {David M. Cerna and Temur Kutsia},
title = {{Unital Anti-Unification: Type and Algorithms}},
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. },
number = {20-02},
year = {2020},
month = {Febrary},
howpublished = {RISC Report},
keywords = {Anti-unification, tree grammars, unital theories, collapse theories},
length = {19},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Cerna]

A Note on Anti-unification and the Theory of Semirings

David M. Cerna

RISC. Technical report, 2020. [pdf]
[bib]
@techreport{RISC6101,
author = {David M. Cerna},
title = {{A Note on Anti-unification and the Theory of Semirings}},
language = {english},
abstract = {It was recently shown that anti-unification over an equational theory consisting of only identity equations (more than one) is nullary. Such pure theories are artificial and are of little effect on practical aspects of anti-unification. In this work, we extend these nullarity results to the theory of semirings, a heavily studied theory with many practical applications. Furthermore, our argument holds over semirings with commutative multiplication and/or idempotent addition. },
year = {2020},
institution = {RISC},
length = {4}
}
[Cerna]

Unital Anti-Unification: Type and Algorithms

David M. Cerna, Temur Kutsia

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. 26:1-26:20. 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, ISBN 978-3-95977-155-9, ISSN 1868-8969. [url]
[bib]
@inproceedings{RISC6132,
author = {David M. Cerna and Temur Kutsia},
title = {{Unital Anti-Unification: Type and Algorithms}},
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 = {26:1--26:20},
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 = {20},
url = {https://drops.dagstuhl.de/opus/volltexte/2020/12352/}
}
[Dramnesc]

Implementation of Deletion Algorithms on Lists and Binary Trees in Theorema

Isabela Dramnesc, Tudor Jebelean

Technical report no. 20-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. April 2020. [pdf]
[bib]
@techreport{RISC6094,
author = {Isabela Dramnesc and Tudor Jebelean},
title = {{Implementation of Deletion Algorithms on Lists and Binary Trees in Theorema}},
language = {english},
number = {20-04},
year = {2020},
month = {April},
length = {25},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[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. [url]
[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}
}
[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, Schloss Hagenberg, 4232 Hagenberg, Austria. 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 = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[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. [url] [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}
}
[Kutsia]

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

Temur Kutsia, Andrew M. Marshall (editors)

Technical report no. 20-10 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2020. [url] [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 = {77},
url = {https://unif2020.org/},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

2019

[Cerna]

Higher-Order Pattern Generalization Modulo Equational Theories

David M. Cerna and Temur Kutsia

2019. [pdf]
[bib]
@techreport{RISC5918,
author = {David M. Cerna and Temur Kutsia},
title = {{Higher-Order Pattern Generalization Modulo Equational Theories}},
language = {english},
abstract = {In this paper we address Three problems related to unital anti-unification. First, we develop a generalalgorithm based on a tree grammar representation of the set of computed generalizations. Secondlywe show that restricting the algorithm to computing linear generalizations only or to term signaturescontaining a single unital function results in a procedure which is minimal complete and Finitary.Thirdly, we show that when the term signature contains two unital functions, unital anti-unification isNullary.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},
length = {40},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Cerna]

A Generic Framework for Higher-Order Generalizations

David M. Cerna, Temur Kutsia

In: Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), Herman Geuvers (ed.), Leibniz International Proceedings in Informatics (LIPIcs) 131, pp. 10:1-10:19. 2019. Schloss Dagstuhl, ISSN 1868-8969. [url]
[bib]
@inproceedings{RISC5947,
author = {David M. Cerna and Temur Kutsia},
title = {{A Generic Framework for Higher-Order Generalizations}},
booktitle = {{Proceedings of the 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019)}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {131},
pages = {10:1--10:19},
publisher = {Schloss Dagstuhl},
isbn_issn = {ISSN 1868-8969},
year = {2019},
editor = {Herman Geuvers},
refereed = {yes},
length = {19},
url = {http://dx.doi.org/10.4230/LIPIcs.FSCD.2019.10}
}
[Cerna]

On the Complexity of Unsatisfiable Primitive Recursively defined $\Sigma_1$-Sentences

David M. Cerna

2019. [pdf]
[bib]
@techreport{RISC5981,
author = {David M. Cerna},
title = {{On the Complexity of Unsatisfiable Primitive Recursively defined $\Sigma_1$-Sentences}},
language = {english},
abstract = {We introduce a measure of complexity based on formula occurrence within instance proofs of an inductive statement. Our measure is closely related to {\em Herbrand Sequent length}, but instead of capturing the number of necessary term instantiations, it captures the finite representational difficulty of a recursive sequence of proofs. We restrict ourselves to a class of unsatisfiable primitive recursively defined negation normal form first-order sentences, referred to as {\em abstract sentences}, which capture many problems of interest; for example, variants of the {\em infinitary pigeonhole principle}. This class of sentences has been particularly useful for inductive formal proof analysis and proof transformation. Together our complexity measure and abstract sentences allow use to capture a notion of {\em tractability} for state-of-the-art approaches to inductive theorem proving, in particular {\em loop discovery} and {\em tree grammar} based inductive theorem provers. We provide a complexity analysis of an important abstract sentence, and discuss the analysis of a few related sentences, based on the infinitary pigeonhole principle which we conjecture represent the upper limits of tractability and foundation of intractability with respect to the current approaches.},
year = {2019},
length = {17},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Cerna]

Idempotent Anti-unification

David Cerna, Temur Kutsia

ACM Transactions on Computational Logic (TOCL) 21(2), pp. 10:1-10:32. 2019. ACM Press, ISSN 1529-3785. [url] [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 = {2019},
refereed = {yes},
length = {32},
url = {https://doi.org/10.1145/3359060}
}
[Dundua]

Variadic Equational Matching

Besik Dundua, Temur Kutsia, Mircea Marin

In: Intelligent Computer Mathematics - 12th International Conference, CICM 2019, Cezary Kaliszyk, Edwin Brady, Andrea Kohlhase, Claudio Sacerdoti Coen (ed.), Lecture Notes in Computer Science 11617, pp. 77-92. 2019. Springer, ISBN 978-3-030-23249-8. [pdf]
[bib]
@inproceedings{RISC5948,
author = {Besik Dundua and Temur Kutsia and Mircea Marin},
title = {{Variadic Equational Matching}},
booktitle = {{Intelligent Computer Mathematics - 12th International Conference, CICM 2019}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {11617},
pages = {77--92},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-23249-8},
year = {2019},
editor = {Cezary Kaliszyk and Edwin Brady and Andrea Kohlhase and Claudio Sacerdoti Coen},
refereed = {yes},
length = {16}
}
[Dundua]

A Rule-based Approach to the Decidability of Safety of ABACα

Mircea Marin, Temur Kutsia, Besik Dundua

In: Proceedings of the 24th ACM Symposium on Access Control Models and Technologies, SACMAT 2019, Florian Kerschbaum, Atefeh Mashatan, Jianwei Niu, Adam J. Lee (ed.), pp. 173-178. 2019. ACM, ISBN 978-1-4503-6753-0. [url] [pdf]
[bib]
@inproceedings{RISC5955,
author = {Mircea Marin and Temur Kutsia and Besik Dundua},
title = {{A Rule-based Approach to the Decidability of Safety of ABACα}},
booktitle = {{Proceedings of the 24th ACM Symposium on Access Control Models and Technologies, SACMAT 2019}},
language = {english},
pages = {173--178},
publisher = {ACM},
isbn_issn = {ISBN 978-1-4503-6753-0},
year = {2019},
editor = {Florian Kerschbaum and Atefeh Mashatan and Jianwei Niu and Adam J. Lee},
refereed = {yes},
length = {6},
url = {https://doi.org/10.1145/3322431.3325416}
}
[Pau]

Computing All Maximal Clique Partitions in a Graph

Temur Kutsia, Cleo Pau

Technical report no. 19-04 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2019. [pdf]
[bib]
@techreport{RISC5939,
author = {Temur Kutsia and Cleo Pau},
title = {{Computing All Maximal Clique Partitions in a Graph}},
language = {english},
number = {19-04},
year = {2019},
length = {9},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Pau]

Solving Proximity Constraints

Temur Kutsia, Cleo Pau

Technical report no. 19-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2019. [pdf]
[bib]
@techreport{RISC5950,
author = {Temur Kutsia and Cleo Pau},
title = {{Solving Proximity Constraints}},
language = {english},
number = {19-06},
year = {2019},
length = {22},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Pau]

Matching and Generalization Modulo Proximity and Tolerance

Temur Kutsia, Cleo Pau

Technical report no. 19-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2019. [pdf]
[bib]
@techreport{RISC5953,
author = {Temur Kutsia and Cleo Pau},
title = {{Matching and Generalization Modulo Proximity and Tolerance}},
language = {english},
number = {19-07},
year = {2019},
length = {5},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Pau]

Solving Proximity Constraints

Temur Kutsia, Cleo Pau

In: Logic-Based Program Synthesis and Transformation - 29th International Symposium, LOPSTR 2019. Revised Selected Papers, Maurizio Gabbrielli (ed.), Lecture Notes in Computer Science 12042, pp. 107-122. 2019. ISBN 978-3-030-45259-9. [pdf]
[bib]
@inproceedings{RISC6100,
author = {Temur Kutsia and Cleo Pau},
title = {{Solving Proximity Constraints}},
booktitle = {{Logic-Based Program Synthesis and Transformation - 29th International Symposium, LOPSTR 2019. Revised Selected Papers}},
language = {english},
series = {Lecture Notes in Computer Science },
volume = {12042},
pages = {107--122},
isbn_issn = {ISBN 978-3-030-45259-9},
year = {2019},
editor = {Maurizio Gabbrielli},
refereed = {yes},
length = {16}
}
[Schreiner]

McCarthy-Kleene fuzzy automata and MSO logics

Manfred Droste, Temur Kutsia, George Rahonis, Wolfgang Schreiner

Information and Computation, pp. -. 2019. Elsevier, ISSN 0890-5401. In Press. [url]
[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 = {2019},
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}
}

2018

[Amiridze]

Anti-Unification and Natural Language Processing

N. Amiridze, T. Kutsia

In: Fifth Workshop on Natural Language and Computer Science, NLCS’18, A. Asudeh, V. de Paiva, L. Moss (ed.), EasyChair preprints 203, pp. 1-12. 2018. [url] [pdf]
[bib]
@inproceedings{RISC5707,
author = {N. Amiridze and T. Kutsia},
title = {{Anti-Unification and Natural Language Processing}},
booktitle = {{Fifth Workshop on Natural Language and Computer Science, NLCS’18}},
language = {english},
series = {EasyChair preprints},
number = {203},
pages = {1--12},
isbn_issn = { },
year = {2018},
editor = {A. Asudeh and V. de Paiva and L. Moss},
refereed = {yes},
length = {12},
url = {https://doi.org/10.29007/fkrh}
}

Loading…