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

2018

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

Term-Graph Anti-Unification

Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret

Technical report no. 18-02 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2018. [pdf]
[bib]
@techreport{RISC5549,
author = {Alexander Baumgartner and Temur Kutsia and Jordi Levy and Mateu Villaret},
title = {{Term-Graph Anti-Unification}},
language = {english},
number = {18-02},
year = {2018},
length = {19},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

Term-Graph Anti-Unification

Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret

In: 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Helene Kirchner (ed.), Leibniz International Proceedings in Informatics (LIPIcs) 108, pp. 9:1-9:17. 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, ISBN 978-3-95977-077-4 ISSN 1868-8969. [url]
[bib]
@inproceedings{RISC5764,
author = {Alexander Baumgartner and Temur Kutsia and Jordi Levy and Mateu Villaret},
title = {{Term-Graph Anti-Unification}},
booktitle = {{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {108},
pages = {9:1--9:17},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
isbn_issn = {ISBN 978-3-95977-077-4 ISSN 1868-8969},
year = {2018},
editor = {Helene Kirchner},
refereed = {yes},
length = {17},
url = {http://drops.dagstuhl.de/opus/volltexte/2018/9179}
}

Idempotent Anti-unification

David M. Cerna Temur Kutsia

RISC. Technical report, Feb. 2018. Submitted for review. [pdf]
[bib]
@techreport{RISC5530,
author = {David M. Cerna Temur Kutsia},
title = {{Idempotent Anti-unification }},
language = {english},
abstract = {In this paper we address two problems related to idempotent anti-unification. First, we show thatthere exists an anti-unification problem with a single idempotent symbol which has an infiniteminimal complete set of generalizations. It means that anti-unification with a single idempotentsymbol has infinitary or nullary generalization type, similar to anti-unification with two idem-potent symbols, shown earlier by Loı̈c Pottier. Next, we develop an algorithm, which takes anarbitrary idempotent anti-unification problem and computes a representation of its solution set inthe form of a regular tree grammar. The algorithm does not depend on the number of idempotentfunction symbols in the input terms. The language generated by the grammar is the minimalcomplete set of generalizations of the given anti-unification problem, which implies that idem-potent anti-unification is infinitary.},
year = {2018},
month = {Feb.},
note = {Submitted for review},
institution = {RISC},
length = {27}
}

Primitive Recursive Proof Systems for Arithmetic

David M. Cerna

RISC. Technical report, January 2018. In revision. [pdf]
[bib]
@techreport{RISC5528,
author = {David M. Cerna},
title = {{Primitive Recursive Proof Systems for Arithmetic}},
language = {english},
abstract = {Peano arithmetic, as formalized by Gentzen, can be presented as an axiom extensionof the LK-calculus with equality and an additional inference rule formalizing induction.While this formalism was enough (with the addition of some meta-theoretic argumentation)to show the consistency of arithmetic, alternative formulations of induction such asthe infinitary ω-rule and cyclic reasoning provide insight into the structure of arithmeticproofs obfuscated by the inference rule formulation of induction. For example, questionsconcerning the elimination of cut, consistency, and proof shape are given more clarity. Thesame could be said for functional interpretations of arithmetic such as system T whichenumerates the recursive functions provably total by arithmetic. A key feature of thesevariations on the formalization of arithmetic is that they get somewhat closer to formalizingthe concept of induction directly using the inferences of the LK-calculus, albeit byadding extra machinery at the meta-level. In this work we present a recursive sequentcalculus for arithmetic which can be syntactically translated into Gentzen formalism ofarithmetic and allows proof normalization to the LK-calculus with equality.},
year = {2018},
month = {January },
note = {In revision},
institution = {RISC},
length = {20}
}

Higher-Order Equational Pattern Anti-Unification

David M. Cerna, Temur Kutsia

In: 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), Helene Kirchner (ed.), Leibniz International Proceedings in Informatics (LIPIcs) 108, pp. 12:1-12:17. 2018. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, ISBN 978-3-95977-077-4 ISSN 1868-8969. [url]
[bib]
@inproceedings{RISC5765,
author = {David M. Cerna and Temur Kutsia},
title = {{Higher-Order Equational Pattern Anti-Unification}},
booktitle = {{3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018)}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {108},
pages = {12:1--12:17},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
isbn_issn = {ISBN 978-3-95977-077-4 ISSN 1868-8969},
year = {2018},
editor = {Helene Kirchner},
refereed = {yes},
length = {17},
url = {http://drops.dagstuhl.de/opus/volltexte/2018/9182}
}

Mechanical Synthesis of Sorting Algorithms for Binary Trees by Logic and Combinatorial Techniques

Isabela Dramnesc, Tudor Jebelean, Sorin Stratulat

Journal of Symbolic Computation 90, pp. 3-41. 2018. Elsevier, 07477171. [url]
[bib]
@article{RISC5715,
author = {Isabela Dramnesc and Tudor Jebelean and Sorin Stratulat},
title = {{Mechanical Synthesis of Sorting Algorithms for Binary Trees by Logic and Combinatorial Techniques}},
language = {english},
journal = {Journal of Symbolic Computation},
volume = {90},
pages = {3--41},
publisher = {Elsevier},
isbn_issn = {07477171},
year = {2018},
refereed = {yes},
keywords = {algorithm synthesis ; automated reasoning ; natural--style proving},
length = {39},
url = {https://doi.org/10.1016/j.jsc.2018.04.002}
}

Pattern-based calculi with finitary matching

Sandra Alves, Besik Dundua, Mário Florido, Temur Kutsia

Logic Journal of the IGPL 26(2), pp. 203-243. 2018. ISSN 1367-0751. [url]
[bib]
@article{RISC5763,
author = {Sandra Alves and Besik Dundua and Mário Florido and Temur Kutsia},
title = {{Pattern-based calculi with finitary matching}},
language = {english},
journal = {Logic Journal of the IGPL},
volume = {26},
number = {2},
pages = {203--243},
isbn_issn = {ISSN 1367-0751},
year = {2018},
refereed = {yes},
length = {41},
url = {https://doi.org/10.1093/JIGPAL/jzx059}
}

Experiments with Automatic Proofs in Elementary Analysis

T. Jebelean

Technical report no. 18-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. April 2018. Work in progress. [pdf] [zip] [pdf]
[bib]
@techreport{RISC5692,
author = {T. Jebelean},
title = {{Experiments with Automatic Proofs in Elementary Analysis}},
language = {english},
abstract = {Combining methods from satisfiability checking with methods from symbolic computation promises to solve challenging problems in various areas of theory and application. We look at the basically equivalent problem of proving statements directly in a non--clausal setting, when additional information on the underlying domain is available in form of specific properties and algorithms.We demonstrate on some concrete examples several heuristic techniques for the automation of natural--style proving of statements from elementary analysis. The purpose of this work in progress is to generate proofs similar to those produced by humans, by combining automated reasoning methods with techniques from computer algebra.Our techniques include: the S-decomposition method for formulae with alternating quantifiers, quantifier elimination by cylindrical algebraic decomposition, analysis of terms behavior in zero, bounding the bounds, rewriting of expressions involving absolute value, algebraic manipulations, and identification of equal terms under unknown functions.These techniques are being implemented in the {\em Theorema} system and are able to construct automatically natural--style proofs for numerous examples including: convergence of sequences, limits and continuity of functions, uniform continuity, and other.},
number = {18-06},
year = {2018},
month = {April},
keywords = {Satisfiability Checking, Natural-style Proofs, Symbolic Computation},
sponsor = {European project ``Satisfiability Checking and Symbolic Computation'' (H2020-FETOPN-2015-CSA 712689)},
length = {33},
type = {Work in progress},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

Idempotent Generalization is Infinitary

David M. Cerna and Temur Kutsia

RISC. Technical report, RISC Report, 2018. [pdf]
[bib]
@techreport{RISC5529,
author = {David M. Cerna and Temur Kutsia},
title = {{Idempotent Generalization is Infinitary}},
language = {english},
abstract = {Let §\mathbf{I}_{S}$ be an equational theory s.t. for each $f\in S$, $f(x,x)=x$. Such an equational theory is said to be {\em idempotent}. It is known that the anti-unification problem (AUP) $f(a,b) \triangleq g(a,b)$ modulo $\mathbf{I}_{\lbrace f,g \rbrace}$ admits infinitely many least-general generalizers (lggs)~\cite{LPottier1989}. We show that, modulo $\mathbf{I}_{\lbrace f\rbrace}$, $f(a,f(a,b)) \triangleq f(b,f(a,b))$ admits infinitely many lggs.},
year = {2018},
howpublished = {RISC Report},
institution = {RISC},
length = {1}
}

Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL

A. Maletzky, F. Immler

In: Intelligent Computer Mathematics (Proceedings of CICM 2018, Hagenberg, Austria, August 13-17), Florian Rabe and William Farmer and Grant Passmore and Abdou Youssef (ed.), Proceedings of CICM 2018, Lecture Notes in Computer Science 11006, pp. 178-193. 2018. Springer, ISBN 978-3-319-96811-7. The final publication is available at Springer via https://doi.org/10.1007/978-3-319-96812-4_16. [url]
[bib]
@inproceedings{RISC5733,
author = {A. Maletzky and F. Immler},
title = {{Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL}},
booktitle = {{Intelligent Computer Mathematics (Proceedings of CICM 2018, Hagenberg, Austria, August 13-17)}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {11006},
pages = {178--193},
publisher = {Springer},
isbn_issn = {ISBN 978-3-319-96811-7},
year = {2018},
note = {The final publication is available at Springer via https://doi.org/10.1007/978-3-319-96812-4_16},
editor = {Florian Rabe and William Farmer and Grant Passmore and Abdou Youssef},
refereed = {yes},
length = {16},
conferencename = {CICM 2018},
url = {https://doi.org/10.1007/978-3-319-96812-4_16}
}

Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL (extended version)

A. Maletzky, F. Immler

RISC, JKU Linz. Technical report, May 2018. arXiv:1805.00304 [cs.LO]. [url]
[bib]
@techreport{RISC5734,
author = {A. Maletzky and F. Immler},
title = {{Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL (extended version)}},
language = {english},
year = {2018},
month = {May},
note = {arXiv:1805.00304 [cs.LO]},
institution = {RISC, JKU Linz},
length = {28},
url = {https://arxiv.org/abs/1805.00304}
}

Proximity-Based Generalization

Temur Kutsia, Cleo Pau

In: 32nd International Workshop on Unification, UNIF 2018, Mauricio Ayala-Rincon and Philippe Balbiani (ed.), pp. - . 2018. [pdf]
[bib]
@inproceedings{RISC5713,
author = {Temur Kutsia and Cleo Pau},
title = {{Proximity-Based Generalization}},
booktitle = {{32nd International Workshop on Unification, UNIF 2018}},
language = {english},
pages = { -- },
isbn_issn = { },
year = {2018},
editor = {Mauricio Ayala-Rincon and Philippe Balbiani},
refereed = {yes},
length = {0}
}

2017

Unranked Second-Order Anti-Unification

Alexander Baumgartner, Temur Kutsia

Information and Computation 255(2), pp. 262-286. 2017. ISSN: 0890-5401. [url]
[bib]
@article{RISC5192,
author = {Alexander Baumgartner and Temur Kutsia},
title = {{Unranked Second-Order Anti-Unification}},
language = {english},
journal = {Information and Computation},
volume = {255},
number = {2},
pages = {262--286},
isbn_issn = {ISSN: 0890-5401},
year = {2017},
refereed = {yes},
length = {25},
url = {http://doi.org/10.1016/j.ic.2017.01.005}
}

Higher-Order Pattern Anti-Unification in Linear Time

Alexander Baumgartner, Temur Kutsia, Jordi Levy, Mateu Villaret

Journal of Automated Reasoning 58(2), pp. 293-310. 2017. ISSN 0168-7433. [url]
[bib]
@article{RISC5337,
author = {Alexander Baumgartner and Temur Kutsia and Jordi Levy and Mateu Villaret},
title = {{Higher-Order Pattern Anti-Unification in Linear Time}},
language = {english},
journal = { Journal of Automated Reasoning},
volume = {58},
number = {2},
pages = {293--310},
isbn_issn = {ISSN 0168-7433},
year = {2017},
refereed = {yes},
length = {18},
url = {http://dx.doi.org/10.1007/s10817-016-9383-3}
}

Gröbner Bases Computation by Triangularizing Macaulay Matrices

Bruno Buchberger

Advanced Studies in Pure Mathematics (The 50th Anniversary of Gröbner Bases) 75, pp. 1-9. 2017. Mathematical Society of Japan, 0.
[bib]
@article{RISC5586,
author = {Bruno Buchberger},
title = {{Gröbner Bases Computation by Triangularizing Macaulay Matrices}},
language = {english},
journal = {Advanced Studies in Pure Mathematics (The 50th Anniversary of Gröbner Bases)},
volume = {75},
pages = {1--9},
publisher = {Mathematical Society of Japan},
isbn_issn = {0},
year = {2017},
refereed = {no},
length = {9}
}

Satisfiability Checking and Symbolic Computation

Abraham Erika , Abbott John , Becker Bernd , Bigatti Anna Maria , Brain Martin , Buchberger Bruno , Cimatti Alessandro , Davenport James , England Matthew , Fontaine Pascal , Forrest Stephen , Griggio Alberto , Kröning Daniel , Seiler Werner M. , Sturm

ACM Communications in Computer Algebra 50(4), pp. 145-147. 2017. 0.
[bib]
@article{RISC5587,
author = { Abraham Erika and Abbott John and Becker Bernd and Bigatti Anna Maria and Brain Martin and Buchberger Bruno and Cimatti Alessandro and Davenport James and England Matthew and Fontaine Pascal and Forrest Stephen and Griggio Alberto and Kröning Daniel and Seiler Werner M. and Sturm },
title = {{Satisfiability Checking and Symbolic Computation}},
language = {english},
journal = {ACM Communications in Computer Algebra},
volume = {50},
number = {4},
pages = {145--147},
isbn_issn = {0},
year = {2017},
refereed = {no},
length = {3}
}

An overview of PρLog

Besik Dundua, Temur Kutsia, Klaus Reisenberger-Hagmayr

In: Proceedings of the 19th International Symposium on Practical Aspects of Declarative Languages, PADL 2017, Y. Lierler and W. Taha (ed.), Lecture Notes in Computer Science 10137, pp. 34-49. 2017. Springer, ISBN 978-3-319-51675-2. [pdf]
[bib]
@inproceedings{RISC5416,
author = {Besik Dundua and Temur Kutsia and Klaus Reisenberger-Hagmayr},
title = {{An overview of PρLog}},
booktitle = {{ Proceedings of the 19th International Symposium on Practical Aspects of Declarative Languages, PADL 2017}},
language = {english},
series = {Lecture Notes in Computer Science},
volume = {10137},
pages = {34--49},
publisher = {Springer},
isbn_issn = {ISBN 978-3-319-51675-2},
year = {2017},
editor = {Y. Lierler and W. Taha},
refereed = {yes},
length = {16}
}

Rewriting Logic from a ρLog Point of View

Mauricio Ayala-Rincon, Besik Dundua, Temur Kutsia, Mircea Marin

In: Proceedings of the 12th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2017) , Sandra Alves and Renata Wasserman (ed.), pp. -. 2017. [pdf]
[bib]
@inproceedings{RISC5473,
author = {Mauricio Ayala-Rincon and Besik Dundua and Temur Kutsia and Mircea Marin},
title = {{Rewriting Logic from a ρLog Point of View}},
booktitle = {{Proceedings of the 12th Workshop on Logical and Semantic Frameworks with Applications (LSFA 2017) }},
language = {english},
pages = {--},
isbn_issn = { },
year = {2017},
editor = {Sandra Alves and Renata Wasserman},
refereed = {yes},
length = {16}
}

Pattern-Based Calculi with Finitary Matching

Sandra Alves, Besik Dundua, Mario Florido, Temur Kutsia

Logic Journal of the IGPL, pp. -. 2017. Oxford University Press, ISSN 1367-0751. To appear. [url]
[bib]
@article{RISC5517,
author = {Sandra Alves and Besik Dundua and Mario Florido and Temur Kutsia},
title = {{Pattern-Based Calculi with Finitary Matching}},
language = {english},
journal = {Logic Journal of the IGPL},
pages = {--},
publisher = {Oxford University Press},
isbn_issn = {ISSN 1367-0751},
year = {2017},
note = {To appear},
refereed = {yes},
length = {41},
url = {https://doi.org/10.1093/JIGPAL/jzx059}
}

Loading…