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

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

### 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]
@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]

### 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, , pp. 1-7. 2020. https://doi.org/10.1145/3341525.3387409.
@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 = {1--7},
isbn_issn = {https://doi.org/10.1145/3341525.3387409},
year = {2020},
editor = {ACM},
refereed = {yes},
length = {7}
}
[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: CSEDU 2020, , pp. 1-8. 2020. not yet known.
@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 = {{CSEDU 2020}},
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 = {1--8},
isbn_issn = {not yet known},
year = {2020},
editor = {Springer},
refereed = {yes},
length = {8}
}
[Cerna]

### Anti-unification and the Theory of Semirings

#### David M. Cerna

RISC / CAS ICS. Technical report, Accepted at the Journal TCS and is in the process of being published., 2020. [pdf]
@techreport{RISC6101,
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.},
year = {2020},
howpublished = {Accepted at the Journal TCS and is in the process of being published.},
institution = {RISC / CAS ICS},
length = {9}
}
[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}
}
[Falkensteiner]

### Power Series Solutions of AODEs - Existence, Uniqueness, Convergence and Computation

#### S. Falkensteiner

RISC Hagenberg, Johannes Kepler University Linz. PhD Thesis. June 2020. Also available as RISC report no. 20-13. [pdf]
@phdthesis{RISC6120,
author = {S. Falkensteiner},
title = {{Power Series Solutions of AODEs - Existence, Uniqueness, Convergence and Computation}},
language = {english},
year = {2020},
month = {June},
note = {Also available as RISC report no. 20-13},
translation = {0},
school = {RISC Hagenberg, Johannes Kepler University Linz},
length = {146}
}
[Goswami]

### On sums of coefficients of polynomials related to the Borwein conjectures

#### Ankush Goswami, Venkata Raghu Tej Pantangi

Technical report no. 20-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. May 2020. [pdf]
@techreport{RISC6113,
author = {Ankush Goswami and Venkata Raghu Tej Pantangi},
title = {{On sums of coefficients of polynomials related to the Borwein conjectures}},
language = {english},
abstract = {Recently, Li (Int. J. Number Theory 2020) obtained an asymptotic formula for a certain partial sum involving coefficients for the polynomial in the First Borwein conjecture. As a consequence, he showed the positivity of this sum. His result was based on a sieving principle discovered by himself and Wan (Sci. China. Math. 2010). In fact, Li points out in his paper that his method can be generalized to prove an asymptotic formula for a general partial sum involving coefficients for any prime $p>3$. In this work, we extend Li's method to obtain asymptotic formula for several partial sums of coefficients of a very general polynomial. We find that in the special cases $p=3, 5$, the signs of these sums are consistent with the three famous Borwein conjectures. Similar sums have been studied earlier by Zaharescu (Ramanujan J. 2006) using a completely different method. We also improve on the error terms in the asymptotic formula for Li and Zaharescu. Using a recent result of Borwein (JNT 1993), we also obtain an asymptotic estimate for the maximum of the absolute value of these coefficients for primes $p=2, 3, 5, 7, 11, 13$ and for $p>15$, we obtain a lower bound on the maximum absolute value of these coefficients for sufficiently large $n$.},
number = {20-07},
year = {2020},
month = {May},
length = {13},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Goswami]

### Some formulae for coefficients in restricted $q$-products

#### Ankush Goswami, Venkata Raghu Tej Pantangi

Technical report no. 20-08 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. May 2020. [pdf]
@techreport{RISC6114,
author = {Ankush Goswami and Venkata Raghu Tej Pantangi},
title = {{Some formulae for coefficients in restricted $q$-products}},
language = {english},
abstract = {In this paper, we derive some formulae involving coefficients of polynomials which occur quite naturally in the study of restricted partitions. Our method involves a recently discovered sieve technique by Li and Wan (Sci. China. Math. 2010). Based on this method, by considering cyclic groups of different orders we obtain some new results for these coefficients. The general result (see Theorem \ref{main00}) holds for any group of the form $\mathbb{Z}_{N}$ where $N\in\mathbb{N}$ and expresses certain partial sums of coefficients in terms of expressions involving roots of unity. By specializing $N$ to different values, we see that these expressions simplify in some cases and we obtain several nice identities involving these coefficients. We also use a result of Sudler (Quarterly J. Math. 1964) to obtain an asymptotic formula for the maximum absolute value of these coefficients.},
number = {20-08},
year = {2020},
month = {May},
length = {11},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Goswami]

### Congruences for generalized Fishburn numbers at roots of unity

#### Ankush Goswami

Technical report no. 20-09 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Schloss Hagenberg, 4232 Hagenberg, Austria. 2020. [pdf]
@techreport{RISC6119,
author = {Ankush Goswami},
title = {{Congruences for generalized Fishburn numbers at roots of unity}},
language = {english},
abstract = {There has been significant recent interest in the arithmeticproperties of the coefficients of $F(1-q)$ and $\mathcal{F}_t(1-q)$where $F(q)$ is the Kontsevich-Zagier strange series and $\mathcal{F}_t(q)$ is the strange series associated to a family of torus knots as studied by Bijaoui, Boden, Myers, Osburn, Rushworth, Tronsgardand Zhou. In this paper, we prove prime power congruences for two families of generalized Fishburn numbers, namely, for the coefficients of $(\zeta_N - q)^s F((\zeta_N - q)^r)$ and $(\zeta_N - q)^s \mathcal{F}_t((\zeta_N -q)^r)$, where $\zeta_N$ is an $N$th root of unity and $r$, $s$ are certain integers.},
number = {20-09},
year = {2020},
length = {17},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Schloss Hagenberg, 4232 Hagenberg, Austria}
}
[Grasegger]

### Computing Animations of Linkages with Rotational Symmetry (Media Exposition)

#### Sean Dewar, Georg Grasegger, Jan Legerský

In: 36th International Symposium on Computational Geometry (SoCG 2020), , Leibniz International Proceedings in Informatics (LIPIcs) 164, pp. 77:1-77:4. 2020. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, Dagstuhl, Germany, ISBN 978-3-95977-143-6. [url]
@inproceedings{RISC6128,
author = {Sean Dewar and Georg Grasegger and Jan Legerský},
title = {{Computing Animations of Linkages with Rotational Symmetry (Media Exposition)}},
booktitle = {{36th International Symposium on Computational Geometry (SoCG 2020)}},
language = {english},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
volume = {164},
pages = {77:1--77:4},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum für Informatik},
isbn_issn = {ISBN 978-3-95977-143-6},
year = {2020},
editor = {Sergio Cabello and Danny Z. Chen},
refereed = {no},
length = {4},
url = {https://doi.org/10.4230/LIPIcs.SoCG.2020.77}
}
[Grasegger]

### Graphs with Flexible Labelings allowing Injective Realizations

#### G. Grasegger, J. Legerský, J. Schicho

Discrete Mathematics 343(6), pp. Art. 111713-. 2020. ISSN 0012-365X. [url]
@article{RISC6012,
author = {G. Grasegger and J. Legerský and J. Schicho},
title = {{Graphs with Flexible Labelings allowing Injective Realizations}},
language = {english},
journal = {Discrete Mathematics},
volume = {343},
number = {6},
pages = {Art. 111713--},
isbn_issn = {ISSN 0012-365X},
year = {2020},
refereed = {yes},
length = {14},
url = {https://doi.org/10.1016/j.disc.2019.111713}
}
[Grasegger]

### On the Classification of Motions of Paradoxically Movable Graphs

#### G. Grasegger, J. Legerský, J. Schicho

arXiv. Technical report, 2020. [url]
@techreport{RISC6092,
author = {G. Grasegger and J. Legerský and J. Schicho},
title = {{On the Classification of Motions of Paradoxically Movable Graphs}},
language = {english},
year = {2020},
institution = {arXiv},
length = {27},
url = {https://arxiv.org/abs/2003.11416}
}
[Grasegger]

### Flexible placements of graphs with rotational symmetry

#### S.Dewar, G. Grasegger, J. Legerský

arXiv. Technical report, 2020. [url]
@techreport{RISC6091,
author = {S.Dewar and G. Grasegger and J. Legerský},
title = {{Flexible placements of graphs with rotational symmetry}},
language = {english},
year = {2020},
institution = {arXiv},
length = {9},
url = {https://arxiv.org/abs/2003.09328}
}