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 ...
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 ...
Publications
2021
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. [url] [pdf]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}
}
2020
Idempotent Anti-unification
David Cerna, Temur Kutsia
ACM Transactions on Computational Logic (TOCL) 21(2), pp. 10:1-10:32. 2020. ACM Press, ISSN 1529-3785. [url] [pdf]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 = {2020},
refereed = {yes},
length = {32},
url = {https://doi.org/10.1145/3359060}
}
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]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/}
}
Higher-order pattern generalization modulo equational theories
David M. Cerna, Temur Kutsia
Mathematical Structures in Computer Science 30(6), pp. 627-663. 2020. ISSN 0960-1295. [url]author = {David M. Cerna and Temur Kutsia},
title = {{Higher-order pattern generalization modulo equational theories}},
language = {english},
journal = {Mathematical Structures in Computer Science},
volume = {30},
number = {6},
pages = {627--663},
isbn_issn = {ISSN 0960-1295},
year = {2020},
refereed = {yes},
length = {37},
url = {https://www.cambridge.org/core/services/aop-cambridge-core/content/view/88E26F155F0FD02B3EDD648971D9AD1B/S0960129520000110a.pdf/higher-order-pattern-generalization-modulo-equational-theories.pdf}
}
Anti-unification and the Theory of Semirings
David M. Cerna
Theor. Comput. Sci. 848, pp. 133-139. 2020. RISC / CAS ICS, 0304-3975. [url]author = {David M. Cerna},
title = {{Anti-unification and the Theory of Semirings}},
language = {english},
abstract = {It was recently shown that anti-unification over an equational theory consisting of only unitequations (more than one) is nullary. Such pure theories are artificial and are of little effect onpractical aspects of anti-unification. In this work, we extend these nullarity results to the theory ofsemirings, a heavily studied theory with many practical applications. Furthermore, our argumentholds over semirings with commutative multiplication and/or idempotent addition. We also cover afew open questions discussed in previous work.},
journal = {Theor. Comput. Sci.},
volume = {848},
pages = {133--139},
isbn_issn = {0304-3975},
year = {2020},
refereed = {yes},
institution = {RISC / CAS ICS},
length = {7},
url = {https://doi.org/10.1016/j.tcs.2020.10.020}
}
Schematic Refutations of Formula Schemata
David Cerna and Alexander Leitsch and Anela Lolic
Journal of Automated Reasoning, pp. -. 2020. 1573-0670. [url]author = {David Cerna and Alexander Leitsch and Anela Lolic},
title = {{Schematic Refutations of Formula Schemata}},
language = {english},
abstract = {Proof schemata are infinite sequences of proofs which are defined inductively. In this paper we present a general framework for schemata of terms, formulas and unifiers and define a resolution calculus for schemata of quantifier-free formulas. The new calculus generalizes and improves former approaches to schematic deduction. As an application of the method we present a schematic refutation formalizing a proof of a weak form of the pigeon hole principle.},
journal = {Journal of Automated Reasoning},
pages = {--},
isbn_issn = {1573-0670},
year = {2020},
refereed = {yes},
length = {47},
url = {https://doi.org/10.1007/s10817-020-09583-8}
}
A Mobile Application for Self-Guided Study of Formal Reasoning
David M. Cerna and Rafael P. D. Kiesel and Alexandra Dzhiganskaya
In: Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2019, Natal, Brazil, 25th August 2019, Pedro Quaresma and Walther Neuper and Jo{ {a}}o Marcos (ed.), EPTCS 313, pp. 35-53. 2020. 2075-2180. [url]author = {David M. Cerna and Rafael P. D. Kiesel and Alexandra Dzhiganskaya},
title = {{A Mobile Application for Self-Guided Study of Formal Reasoning}},
booktitle = {{Proceedings 8th International Workshop on Theorem Proving Components for Educational Software, ThEdu@CADE 2019, Natal, Brazil, 25th August 2019}},
language = {english},
abstract = {In this work, we introduce AXolotl, a self-study aid designed to guide students through the basics of formal reasoning and term manipulation. Unlike most of the existing study aids for formal reasoning, AXolotl is an Android-based application with a simple touch-based interface. Part of the design goal was to minimize the possibility of user errors which distract from the learning process. Such as typos or inconsistent application of the provided rules. The system includes a zoomable proof viewer which displays the progress made so far and allows for storage of the completed proofs as a JPEG or LaTeX file. The software is available on the google play store and comes with a small library of problems. Additional problems may be opened in AXolotl using a simple input language. Currently, AXolotl supports problems that can be solved using rules which transform a single expression into a set of expressions. This covers educational scenarios found in our first-semester introduction to logic course and helps bridge the gap between propositional and first-order reasoning. Future developments will include rewrite rules which take a set of expressions and return a set of expressions, as well as a quantified first-order extension.},
series = {EPTCS},
volume = {313},
pages = {35--53},
isbn_issn = {2075-2180},
year = {2020},
editor = {Pedro Quaresma and Walther Neuper and Jo{~{a}}o Marcos},
refereed = {yes},
length = {19},
url = {https://doi.org/10.4204/EPTCS.313.3}
}
Unital Anti-Unification: Type and Algorithms
David M. Cerna , Temur Kutsia
In: 5th International Conference on Formal Structures for Computation and Deduction, {FSCD} 2020, June 29-July 6, 2020, Paris, France (Virtual Conference, Zena M. Ariola (ed.), Proceedings of FSCD, LIPICS 16720-02, pp. 1-20. 2020. 1868-8969. [url]author = {David M. Cerna and Temur Kutsia},
title = {{Unital Anti-Unification: Type and Algorithms}},
booktitle = {{5th International Conference on Formal Structures for Computation and Deduction, {FSCD} 2020, June 29-July 6, 2020, Paris, France (Virtual Conference}},
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. },
series = {LIPICS},
volume = {167},
number = {20-02},
pages = {1--20},
isbn_issn = {1868-8969},
year = {2020},
editor = {Zena M. Ariola},
refereed = {yes},
keywords = {Anti-unification, tree grammars, unital theories, collapse theories},
length = {19},
conferencename = {FSCD},
url = {https://doi.org/10.4230/LIPIcs.FSCD.2020.26}
}
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]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}
}
Synthesis of Delete on Lists and Binary Trees Using Multisets in Theorema
Isabela Dramnesc, Tudor Jebelean
Technical report no. 20-15 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. September 2020. [pdf]author = {Isabela Dramnesc and Tudor Jebelean},
title = {{Synthesis of Delete on Lists and Binary Trees Using Multisets in Theorema}},
language = {English},
abstract = {We demonstrate the deduction based synthesis of element deletion algorithms for[sorted] lists and [sorted] binary trees, by first developing the necessary theory which ismulti–type: basic ordered elements, multisets, lists, and trees. The generated algorithms are“pattern matching”, namely sets of conditional equalities, and we also demonstrate theirtransformation into functional algorithms and, for lists, into tail recursive algorithms. Thiswork constitutes a case study first in theory exploration and second in automated synthesisand transformation of algorithms synthesized on the basis of natural style proofs, whichallows to investigate the heuristics of theory construction on multiple types, as well as thenatural style inferences and strategies for constructing human readable synthesis proofs. Theexperiments are performed in the frame of the Theorema system.},
number = {20-15},
year = {2020},
month = {September},
keywords = {automated reasoning; algorithm synthesis; lists; binary trees; multisets; Theorema},
length = {22},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
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]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}
}
Extending the 𝜌Log Calculus with Proximity Relations
Besik Dundua, Temur Kutsia, Mircea Marin, Cleo Pau
In: AMINSE 2019: Applications of Mathematics and Informatics in Natural Sciences and Engineering, George Jaiani, David Natroshvili (ed.), Springer Proceedings in Mathematics & Statistics 334, pp. 83-100. 2020. Springer, ISBN 978-3-030-56356-1, 978-3-030-56355-4. [url] [pdf]author = {Besik Dundua and Temur Kutsia and Mircea Marin and Cleo Pau},
title = {{Extending the 𝜌Log Calculus with Proximity Relations}},
booktitle = {{AMINSE 2019: Applications of Mathematics and Informatics in Natural Sciences and Engineering}},
language = {english},
series = {Springer Proceedings in Mathematics & Statistics},
volume = {334},
pages = {83--100},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-56356-1, 978-3-030-56355-4},
year = {2020},
editor = {George Jaiani and David Natroshvili},
refereed = {yes},
length = {18},
url = {https://doi.org/10.1007/978-3-030-56356-1_6}
}
Specification and Analysis of ABAC Policies in a Rule-Based Framework
Besik Dundua, Temur Kutsia, Mircea Marin, Mikheil Rukhaia
In: AMINSE 2019: Applications of Mathematics and Informatics in Natural Sciences and Engineering, George Jaiani, David Natroshvili (ed.), Springer Proceedings in Mathematics & Statistics 334, pp. 101-116. 2020. Springer, ISBN 978-3-030-56356-1, 978-3-030-56355-4. [url] [pdf]author = {Besik Dundua and Temur Kutsia and Mircea Marin and Mikheil Rukhaia},
title = {{Specification and Analysis of ABAC Policies in a Rule-Based Framework}},
booktitle = {{AMINSE 2019: Applications of Mathematics and Informatics in Natural Sciences and Engineering}},
language = {english},
series = {Springer Proceedings in Mathematics & Statistics},
volume = {334},
pages = {101--116},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-56356-1, 978-3-030-56355-4},
year = {2020},
editor = {George Jaiani and David Natroshvili},
refereed = {yes},
length = {16},
url = {https://doi.org/10.1007/978-3-030-56356-1_7}
}
A Rule-Based System for Computation and Deduction in Mathematica
Mircea Marin, Besik Dundua, Temur Kutsia
In: WRLA 2020: Rewriting Logic and Its Applications, Santiago Escobar, Narciso Martí-Oliet (ed.), Lecture Notes in Computer Science 12328, pp. 57-74. 2020. Springer, ISBN 978-3-030-63595-4, 978-3-030-63594-7. [url] [pdf]author = {Mircea Marin and Besik Dundua and Temur Kutsia},
title = {{A Rule-Based System for Computation and Deduction in Mathematica}},
booktitle = {{WRLA 2020: Rewriting Logic and Its Applications}},
language = {english},
series = { Lecture Notes in Computer Science},
volume = {12328},
pages = {57--74},
publisher = {Springer},
isbn_issn = {ISBN 978-3-030-63595-4, 978-3-030-63594-7},
year = {2020},
editor = {Santiago Escobar and Narciso Martí-Oliet},
refereed = {yes},
length = {18},
url = {https://doi.org/10.1007/978-3-030-63595-4_4}
}
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]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}
}
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]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}
}
Proceedings of The 34th International Workshop on Unification, UNIF 2020
Temur Kutsia and 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. [pdf]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 = {82},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
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. [url]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}
}
2019
Higher-Order Pattern Generalization Modulo Equational Theories
David M. Cerna and Temur Kutsia
Submitted to the RISC Report Series. 2019. [pdf]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}
}
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]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}
}