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

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

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

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

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

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