## Publications

[Legersky]

### On the maximal number of real embeddings of minimally rigid graphs in R2, R3 and S2

#### E. Bartzos, I.Z. Emiris, J. Legerský, E. Tsigaridas

Journal of Symbolic Computation 102, pp. 189-208. 2021. ISSN 0747-7171. [url]
@article{RISC5992,
author = {E. Bartzos and I.Z. Emiris and J. Legerský and E. Tsigaridas},
title = {{On the maximal number of real embeddings of minimally rigid graphs in R2, R3 and S2}},
language = {english},
journal = {Journal of Symbolic Computation},
volume = {102},
pages = {189--208},
isbn_issn = {ISSN 0747-7171},
year = {2021},
refereed = {yes},
length = {20},
url = {https://doi.org/10.1016/j.jsc.2019.10.015}
}
[Maletzky]

### A generic and executable formalization of signature-based Gröbner basis algorithms

#### Alexander Maletzky

J. Symb. Comput. 106, pp. 23-47. 2021. Elsevier, ISSN 0747-7171. arXiv:2012.02239 [cs.SC], https://doi.org/10.1016/j.jsc.2020.12.001. [url]
@article{RISC6225,
author = {Alexander Maletzky},
title = {{A generic and executable formalization of signature-based Gröbner basis algorithms}},
language = {english},
journal = {J. Symb. Comput.},
volume = {106},
pages = {23--47},
publisher = {Elsevier},
isbn_issn = {ISSN 0747-7171},
year = {2021},
note = {arXiv:2012.02239 [cs.SC], https://doi.org/10.1016/j.jsc.2020.12.001},
refereed = {yes},
length = {25},
url = {https://arxiv.org/abs/2012.02239}
}
[Schneider]

### The Polarized Transition Matrix Element $A_{g, q}(N)$ of the Variable Flavor Number Scheme at $O(\alpha_s^3)$

#### A. Behring, J. Blümlein, A. De Freitas, A. von Manteuffel, K. Schönwald, and C. Schneider

Technical report no. 21-01 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2021. Available also under arXiv:2101.05733 [hep-ph]. [pdf]
@techreport{RISC6250,
author = {A. Behring and J. Blümlein and A. De Freitas and A. von Manteuffel and K. Schönwald and and C. Schneider},
title = {{The Polarized Transition Matrix Element $A_{g,q}(N)$ of the Variable Flavor Number Scheme at $O(\alpha_s^3)$}},
language = {english},
number = {21-01},
year = {2021},
note = {Available also under arXiv:2101.05733 [hep-ph]},
length = {25},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}

[Ablinger]

### Proving Two Conjectural Series for $\zeta(7)$ and Discovering More Series for $\zeta(7)$

#### J. Ablinger

In: Mathematical Aspects of Computer and Information Science, , pp. 42-47. 2020. Springer International Publishing, 978-3-030-43120-4. [url]
@inproceedings{RISC6102,
author = {J. Ablinger},
title = {{Proving Two Conjectural Series for $\zeta(7)$ and Discovering More Series for $\zeta(7)$}},
booktitle = {{Mathematical Aspects of Computer and Information Science}},
language = {english},
pages = {42--47},
publisher = {Springer International Publishing},
isbn_issn = {978-3-030-43120-4},
year = {2020},
editor = {D. Slamanig and E. Tsigaridas and Z. Zafeirakopoulos},
refereed = {yes},
length = {6},
url = {https://arxiv.org/abs/1908.06631v1}
}
[Ablinger]

### Subleading logarithmic QED initial state corrections to $e^+e^−\to γ^⁎/Z^{0⁎}$ to $O(\alpha^6L^5)$

#### J. Ablinger, J. Blümlein, A. De Freitas, K. Schönwald

Nuclear Physics B 955, pp. 115045-115045. 2020. ISSN 0550-3213. [url]
@article{RISC6111,
author = {J. Ablinger and J. Blümlein and A. De Freitas and K. Schönwald},
title = {{Subleading logarithmic QED initial state corrections to $e^+e^−\to γ^⁎/Z^{0⁎}$ to $O(\alpha^6L^5)$}},
language = {english},
journal = {Nuclear Physics B},
volume = {955},
pages = {115045--115045},
isbn_issn = { ISSN 0550-3213},
year = {2020},
refereed = {yes},
length = {0},
url = {http://www.sciencedirect.com/science/article/pii/S0550321320301310}
}
[Banerjee]

### Hook Type Tableaux and Partition Identities

#### Koustav Banerjee, Manosij Ghosh Dastidar

Research Institute for Symbolic Computation. Technical report, 2020. Preprint. [pdf]
@techreport{RISC6118,
author = {Koustav Banerjee and Manosij Ghosh Dastidar},
title = {{Hook Type Tableaux and Partition Identities}},
language = {english},
abstract = {In this paper we exhibit the box-stacking principle (BSP) in conjunction with Young diagrams to prove generalizations of the Stanley’s and Elder’s theorem without the use of partition statistics in general. We explain how the principle can be used to prove another interesting theorem on partitions with parts separated by parity, a special case of which is George Andrews’s result in [2].},
year = {2020},
note = {Preprint},
institution = {Research Institute for Symbolic Computation},
length = {19}
}
[Capco]

### Robots, computer algebra and 8 connected components

#### J. Capco, M. Safey el Din, J. Schicho

In: Proceedings of ISSAC 2020, , pp. 62-69. 2020. 978-1-4503-7100-1. [url]
@inproceedings{RISC6247,
author = {J. Capco and M. Safey el Din and J. Schicho},
title = {{Robots, computer algebra and 8 connected components}},
booktitle = {{Proceedings of ISSAC 2020}},
language = {english},
pages = {62--69},
isbn_issn = {978-1-4503-7100-1},
year = {2020},
editor = {I. Emiris and L. Zhi},
refereed = {yes},
length = {8},
url = {https://arxiv.org/abs/2008.13392}
}
[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), , 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]
@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/}
}
[Cerna]

### 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]
@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 = {2020},
refereed = {yes},
length = {32},
url = {https://doi.org/10.1145/3359060}
}
[Cerna]

### Aiding an Introduction to Formal Reasoning Within a First-Year Logic Course for CS Majors Using a Mobile Self-Study App

#### David M. Cerna, Martina Seidl, Wolfgang Schreiner, Wolfgang Windsteiger, Armin Biere

In: ITICSE 2020, , Proceedings of ITICSE, pp. 61-67. 2020. 9781450368742. [url]
@inproceedings{RISC6096,
author = {David M. Cerna and Martina Seidl and Wolfgang Schreiner and Wolfgang Windsteiger and Armin Biere},
title = {{Aiding an Introduction to Formal Reasoning Within a First-Year Logic Course for CS Majors Using a Mobile Self-Study App}},
booktitle = {{ITICSE 2020}},
language = {english},
abstract = {In this paper, we share our experiences concerning the introduc-tion of the Android-based self-study app AXolotl within the first-semester logic course offered at our university. This course is manda-tory for students majoring in Computer Science and Artificial In-telligence. AXolotl was used as part of an optional lab assignmentbridging clausal reasoning and SAT solving with classical reason-ing, proof construction, and first-order logic. The app provides anintuitive interface for proof construction in various logical calculiand aids the students through rule application. The goal of thelab assignment was to help students make a smoother transitionfrom clausal and decompositional reasoning used earlier in thecourse to inferential and contextual reasoning required for proofconstruction and first-order logic. We observed that the lab had apositive influence on students’ understanding and end the paperwith a discussion of these results.},
pages = {61--67},
isbn_issn = {9781450368742},
year = {2020},
editor = {ACM},
refereed = {yes},
length = {7},
conferencename = {ITICSE},
url = {https://dl.acm.org/doi/10.1145/3341525.3387409}
}
[Cerna]

### Computational Logic in the First Semester of Computer Science: An Experience Report

#### David M. Cerna, Martina Seidl, Wolfgang Schreiner, Wolfgang Windsteiger, Armin Biere

In: Proceedings of the 12th International Conference on Computer Supported Education - Volume 2: CSEDU, , Proceedings of CSEDU, pp. 374-381. 2020. 978-989-758-417-6. [url]
@inproceedings{RISC6097,
author = {David M. Cerna and Martina Seidl and Wolfgang Schreiner and Wolfgang Windsteiger and Armin Biere},
title = {{Computational Logic in the First Semester of Computer Science: An Experience Report}},
booktitle = {{Proceedings of the 12th International Conference on Computer Supported Education - Volume 2: CSEDU}},
language = {english},
abstract = {Nowadays, logic plays an ever-increasing role in modern computer science, in theory as well as in practice.Logic forms the foundation of the symbolic branch of artificial intelligence and from an industrial perspective,logic-based verification technologies are crucial for major hardware and software companies to ensure thecorrectness of complex computing systems. The concepts of computational logic that are needed for such purposes are often avoided in early stages of computer science curricula. Instead, classical logic education mainlyfocuses on mathematical aspects of logic depriving students to see the practical relevance of this subject. Inthis paper we present our experiences with a novel design of a first-semester bachelor logic course attendedby about 200 students. Our aim is to interlink both foundations and applications of logic within computerscience. We report on our experiences and the feedback we got from the students through an extensive surveywe performed at the end of the semester.},
pages = {374--381},
isbn_issn = {978-989-758-417-6},
year = {2020},
editor = {Springer},
refereed = {yes},
length = {8},
conferencename = {CSEDU},
}
[Cerna]

### Anti-unification and the Theory of Semirings

#### David M. Cerna

Theor. Comput. Sci. 848, pp. 133-139. 2020. RISC / CAS ICS, 0304-3975. [url]
@article{RISC6234,
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}
}
[Cerna]

### Schematic Refutations of Formula Schemata

#### David Cerna and Alexander Leitsch and Anela Lolic

Journal of Automated Reasoning, pp. -. 2020. 1573-0670. [url]
@article{RISC6235,
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}
}
[Cerna]

### 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]
@article{RISC6226,
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},
}
[Cerna]

### 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, , EPTCS 313, pp. 35-53. 2020. 2075-2180. [url]
@inproceedings{RISC6236,
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}
}
[Cerna]

### 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, , Proceedings of FSCD, LIPICS 167/20-02, pp. 1-20. 2020. 1868-8969. [url]
@inproceedings{RISC6237,
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}
}
[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]
@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}
}
[Dramnesc]

### 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]
@techreport{RISC6206,
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}
}
[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), , 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]
@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}
}
[Dundua]

### 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, , Springer Proceedings in Mathematics & Statistics 334, pp. 101-116. 2020. Springer, ISBN 978-3-030-56356-1, 978-3-030-56355-4. [url] [pdf]
@incollection{RISC6228,
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}
}