RISC PhD Fellowships 2017

Project Lead

Project Duration

01/01/2017 - 31/12/2017

Publications

2025

[Schneider]

Creative Telescoping for Hypergeometric Double Sums

P. Paule, C. Schneider

J. Symb. Comput. 128(102394), pp. 1-30. 2025. ISSN: 0747-7171. Symbolic Computation and Combinatorics: A special issue in memory and honor of Marko Petkovšek, edited by Shaoshi Chen, Sergei Abramov, Manuel Kauers, Eugene Zima. [doi]
[bib]
@article{RISC7068,
author = {P. Paule and C. Schneider},
title = {{Creative Telescoping for Hypergeometric Double Sums}},
language = {english},
abstract = {We present efficient methods for calculating linear recurrences of hypergeometric double sums and, more generally, of multiple sums. In particular, we supplement this approach with the algorithmic theory of contiguous relations, which guarantees the applicability of our method for many input sums. In addition, we elaborate new techniques to optimize the underlying key task of our method to compute rational solutions of parameterized linear recurrences.},
journal = {J. Symb. Comput.},
volume = {128},
number = {102394},
pages = {1--30},
isbn_issn = {ISSN: 0747-7171},
year = {2025},
note = {Symbolic Computation and Combinatorics: A special issue in memory and honor of Marko Petkovšek, edited by Shaoshi Chen, Sergei Abramov, Manuel Kauers, Eugene Zima},
refereed = {yes},
keywords = {creative telescoping; symbolic summation, hypergeometric multi-sums, contiguous relations, parameterized recurrences, rational solutions},
length = {30},
url = {https://doi.org/10.1016/j.jsc.2024.102394}
}

2024

[AUTHOR]

Proximity-based matching with arbitrary T-norms

Maximilian Donnermair

RISC, Johannes Kepler University Linz. Bachelor Thesis. 2024. [pdf]
[bib]
@misc{RISC7061,
author = {Maximilian Donnermair},
title = {{Proximity-based matching with arbitrary T-norms}},
language = {english},
year = {2024},
translation = {0},
institution = {RISC, Johannes Kepler University Linz},
length = {38}
}
[Cerna]

Equational Anti-unification over Absorption Theories

Mauricio Ayala-Rincón, David M. Cerna, Andres Felipe Gonzalez Barragan, Temur Kutsia

In: Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Christoph Benzmüller, Marijn J. H. Heule, Renate A. Schmidt (ed.), Lecture Notes in Artificial Intelligence 14740, pp. 317-337. 2024. Springer, ISBN 978-3-031-63500-7. [doi]
[bib]
@inproceedings{RISC7064,
author = {Mauricio Ayala-Rincón and David M. Cerna and Andres Felipe Gonzalez Barragan and Temur Kutsia},
title = {{Equational Anti-unification over Absorption Theories}},
booktitle = {{Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings}},
language = {english},
series = {Lecture Notes in Artificial Intelligence},
volume = {14740},
pages = {317--337},
publisher = {Springer},
isbn_issn = {ISBN 978-3-031-63500-7},
year = {2024},
editor = {Christoph Benzmüller and Marijn J. H. Heule and Renate A. Schmidt},
refereed = {yes},
length = {21},
url = {https://doi.org/10.1007/978-3-031-63501-4_17}
}
[de Freitas]

The first-order factorizable contributions to the three-loop massive operator matrix elements $A_{Qg}^{(3)}$ and $Delta A_{Qg}^{(3)}$

J. Ablinger, A. Behring, J. Bluemlein, A. De Freitas, A. von Manteuffel, C. Schneider, K. Schoenwald

Nuclear Physics B 999(116427), pp. 1-42. 2024. ISSN 0550-3213. arXiv:2311.00644 [hep-ph]. [doi]
[bib]
@article{RISC6755,
author = {J. Ablinger and A. Behring and J. Bluemlein and A. De Freitas and A. von Manteuffel and C. Schneider and K. Schoenwald},
title = {{The first--order factorizable contributions to the three--loop massive operator matrix elements $A_{Qg}^{(3)}$ and $Delta A_{Qg}^{(3)}$}},
language = {english},
abstract = {The unpolarized and polarized massive operator matrix elements $A_{Qg}^{(3)}$ and $Delta A_{Qg}^{(3)}$contain first--order factorizable and non--first--order factorizable contributions in the determining difference or differential equations of their master integrals. We compute their first--order factorizable contributions in the single heavy mass case for all contributing Feynman diagrams. Moreover, we present the complete color--$zeta$ factors for the cases in which also non--first--order factorizable contributions emerge in the master integrals, but cancel in the final result as found by using the method of arbitrary high Mellin moments. Individual contributions depend also on generalized harmonic sums and on nested finite binomial and inverse binomial sums in Mellin $N$--space, and correspondingly, on Kummer--Poincar'e and square--root valued alphabets in Bjorken--$x$ space. We present a complete discussion of the possibilities of solving the present problem in $N$--space analytically and we also discuss the limitations in the present case to analytically continue the given $N$--space expressions to $N in mathbb{C}$ by strict methods. The representation through generating functions allows a well synchronized representation of the first--order factorizable results over a 17--letter alphabet. We finally obtain representations in terms of iterated integrals over the corresponding alphabet in $x$--space, also containing up to weight {sf w = 5} special constants, which can be rationalized to Kummer--Poincar'e iterated integrals at special arguments. The analytic $x$--space representation requires separate analyses for the intervals $x in [0,1/4], [1/4,1/2], [1/2,1]$ and $x > 1$. We also derive the small and large $x$ limits of the first--order factorizable contributions. Furthermore, we perform comparisons to a number of known Mellin moments, calculated by a different method for the corresponding subset of Feynman diagrams, and an independent high--precision numerical solution of the problems.},
journal = {Nuclear Physics B},
volume = {999},
number = {116427},
pages = {1--42},
isbn_issn = {ISSN 0550-3213},
year = {2024},
note = {arXiv:2311.00644 [hep-ph]},
refereed = {yes},
keywords = {Feynman diagram, massive operator matrix elements, computer algebra, differential equations, difference equations, coupled systems, nested integrals, nested sums},
length = {42},
url = {https://doi.org/10.1016/j.nuclphysb.2023.116427}
}
[de Freitas]

The non-first-order-factorizable contributions to the three-loop single-mass operator matrix elements $A_{Qg}^{(3)}$ and $Delta A_{Qg}^{(3)}$

J. Ablinger, A. Behring, J. Bluemlein, A. De Freitas, A. von Manteuffel, C. Schneider, K. Schoenwald

Physics Letter B 854(138713), pp. 1-8. 2024. ISSN 0370-2693. arXiv:2403.00513 [[hep-ph]. [doi]
[bib]
@article{RISC7058,
author = {J. Ablinger and A. Behring and J. Bluemlein and A. De Freitas and A. von Manteuffel and C. Schneider and K. Schoenwald},
title = {{The non-first-order-factorizable contributions to the three-loop single-mass operator matrix elements $A_{Qg}^{(3)}$ and $Delta A_{Qg}^{(3)}$}},
language = {english},
abstract = {The non-first-order-factorizable contributions to the unpolarized and polarized massive operator matrix elements to three-loop order, $A_{Qg}^{(3)}$ and $Delta A_{Qg}^{(3)}$, are calculated in the single-mass case. For the $_2F_1$-related master integrals of the problem, we use a semi-analytic method basedon series expansions and utilize the first-order differential equations for the master integrals whichdoes not need a special basis of the master integrals. Due to the singularity structure of this basis a part of the integrals has to be computed to $O(ep^5)$ in the dimensional parameter. The solutions have to be matched at a series of thresholds and pseudo-thresholds in the region of the Bjorken variable $x in ]0,infty[$ using highly precise series expansions to obtain the imaginary part of the physical amplitude for $x in ]0,1]$ at a high relative accuracy. We compare the present results both with previous analytic results, the results for fixed Mellin moments, and a prediction in the small-$x$ region. We also derive expansions in the region of small and large values of $x$. With this paper, all three-loop single-mass unpolarized and polarized operator matrix elements are calculated.},
journal = {Physics Letter B},
volume = {854},
number = {138713},
pages = {1--8},
isbn_issn = {ISSN 0370-2693},
year = {2024},
note = {arXiv:2403.00513 [[hep-ph]},
refereed = {yes},
keywords = {Feynman diagram, massive operator matrix elements, computer algebra, differential equations, difference equations, coupled systems, numerics},
length = {8},
url = {https://doi.org/10.1016/j.physletb.2024.138713}
}
[de Freitas]

Challenges for analytic calculations of the massive three-loop form factors

J Bluemlein, A. De Freitas, P. Marquard, C. Schneider

In: Proceedings of Loops and Legs in Quantum Field Theory, P. Marquard, M. Steinhauser (ed.)PoS(LL2024)031/24-05, pp. 1-18. 2024. ISSN 1824-8039. arXiv:2408.07046 [hep-ph]. [doi]
[bib]
@inproceedings{RISC7066,
author = {J Bluemlein and A. De Freitas and P. Marquard and C. Schneider},
title = {{Challenges for analytic calculations of the massive three-loop form factors}},
booktitle = {{Proceedings of Loops and Legs in Quantum Field Theory}},
language = {english},
abstract = {The calculation of massive three-loop QCD form factors using in particular the large moments method has been successfully applied to quarkonic contributions in [1]. We give a brief review of the different steps of the calculation and report on improvements of our methods that enabled us to push forward the calculations of the gluonic contributions to the form factors.},
volume = {PoS(LL2024)031},
number = {24-05},
pages = {1--18},
isbn_issn = {ISSN 1824-8039},
year = {2024},
note = { arXiv:2408.07046 [hep-ph]},
editor = {P. Marquard and M. Steinhauser},
refereed = {no},
keywords = {Form factor; computer algebra, coupled systems, differential equations, recurrences, analytic continuation, holonomic functions},
length = {18},
url = {https://doi.org/10.22323/1.467.0031 }
}
[de Freitas]

The three-loop single-mass heavy flavor corrections to deep-inelastic scattering

J. Ablinger, A. Behring, J. Bluemlein, A. De Freitas, A. von Manteuffel, C. Schneider, K. Schoenwald

In: Proceedings of Loops and Legs in Quantum Field Theory, P. Marquard, M. Steinhauser (ed.)PoS(LL2024)047 , pp. 1-12. 2024. SSN 1824-8039. arXiv:2407.02006 [hep-ph]. [doi]
[bib]
@inproceedings{RISC7067,
author = {J. Ablinger and A. Behring and J. Bluemlein and A. De Freitas and A. von Manteuffel and C. Schneider and K. Schoenwald},
title = {{The three-loop single-mass heavy flavor corrections to deep-inelastic scattering}},
booktitle = {{Proceedings of Loops and Legs in Quantum Field Theory}},
language = {english},
abstract = {We report on the status of the calculation of the massive Wilson coefficients and operator matrix elements for deep-inelastic scatterung to three-loop order. We discuss both the unpolarized and the polarized case, for which all the single-mass and nearly all two-mass contributions have been calculated. Numerical results on the structure function $F_2(x,Q^2)$ are presented. In the polarized case, we work in the Larinscheme and refer to parton distribution functions in this scheme. Furthermore, results on the three-loop variable flavor number scheme are presented.},
volume = {PoS(LL2024)047 },
pages = {1--12},
isbn_issn = {SSN 1824-8039},
year = {2024},
note = {arXiv:2407.02006 [hep-ph]},
editor = {P. Marquard and M. Steinhauser},
refereed = {no},
keywords = {Feynman integrals, deep-inelastic scattering, numerical results},
length = {12},
url = {https://doi.org/10.22323/1.467.0047 }
}
[Ehling]

Solving Quantitative Equations

G. Ehling, T. Kutsia

Technical report no. 24-03 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). April 2024. Licensed under CC BY 4.0 International. [doi] [pdf]
[bib]
@techreport{RISC7056,
author = {G. Ehling and T. Kutsia},
title = {{Solving Quantitative Equations}},
language = {english},
abstract = {Quantitative equational reasoning provides a framework that extends equality to an abstract notion of proximity by endowing equations with an element of a quantale. In this paper, we discuss the unification problem for a special class of shallow subterm-collapse-free quantitative equational theories. We outline rule-based algorithms for solving such equational unification problems over generic as well as idempotent Lawvereian quantales and study their properties.},
number = {24-03},
year = {2024},
month = {April},
keywords = {quantitative equational reasoning, Lawvereian quantales, equational unification},
length = {23},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Ehling]

Solving Quantitative Equations

Georg Ehling, Temur Kutsia

In: Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Christoph Benzmüller, Marijn J. H. Heule, Renate A. Schmidt (ed.), Lecture Notes in Artificial Intelligence 14740, pp. 381-400. 2024. Springer, ISBN 978-3-031-63500-7. [doi]
[bib]
@inproceedings{RISC7065,
author = {Georg Ehling and Temur Kutsia},
title = {{Solving Quantitative Equations}},
booktitle = {{Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings}},
language = {english},
series = {Lecture Notes in Artificial Intelligence},
volume = {14740},
pages = {381--400},
publisher = {Springer},
isbn_issn = {ISBN 978-3-031-63500-7},
year = {2024},
editor = {Christoph Benzmüller and Marijn J. H. Heule and Renate A. Schmidt},
refereed = {yes},
length = {20},
url = {https://doi.org/10.1007/978-3-031-63501-4_20}
}
[Obrovsky]

Maximum-order Complexity and 2-Adic Complexity

Z. Chen, Z. Chen, J. Obrovsky, A. Winterhof

IEEE Transactions on Information Theory 70(8), pp. 6060-6067. 2024. ISSN: 0018-9448. [doi]
[bib]
@article{RISC7060,
author = {Z. Chen and Z. Chen and J. Obrovsky and A. Winterhof},
title = {{Maximum-order Complexity and 2-Adic Complexity}},
language = {english},
abstract = {The 2-adic complexity has been well-analyzed in the periodic case. However, we are not aware of any theoretical results in the aperiodic case. In particular, the Nth 2-adic complexity has not been studied for any promising candidate of a pseudorandom sequence of finite length N. Also nothing seems be known for a part of the period of length N of any cryptographically interesting periodic sequence. Here we introduce the first method for this aperiodic case. More precisely, we study the relation between Nth maximum-order complexity and Nth 2-adic complexity of binary sequences and prove a lower bound on the Nth 2-adic complexity in terms of the Nth maximum-order complexity. Then any known lower bound on the Nth maximum-order complexity implies a lower bound on the Nth 2-adic complexity of the same order of magnitude. In the periodic case, one can prove a slightly better result. The latter bound is sharp, which is illustrated by the maximum-order complexity of ell -sequences. The idea of the proof helps us to characterize the maximum-order complexity of periodic sequences in terms of the unique rational number defined by the sequence. We also show that a periodic sequence of maximal maximum-order complexity must be also of maximal 2-adic complexity.},
journal = {IEEE Transactions on Information Theory},
volume = {70},
number = {8},
pages = { 6060--6067},
isbn_issn = {ISSN: 0018-9448},
year = {2024},
refereed = {yes},
keywords = {Complexity theory;Polynomials;Random sequences;Cryptography;Surveys;Shift registers;Mathematics;Pseudorandom sequences;maximum-order complexity;2-adic complexity;ℓ-sequences},
length = {8},
url = {https://doi.org/10.1109/TIT.2024.3405946}
}
[Qi]

A tree-based algorithm for the integration of monomials in the Chow ring of the moduli space of stable marked curves of genus zero

Jiayue Qi

Journal of Symbolic Computation 122(102253), pp. -. 2024. ISSN: 0747-7171. [doi]
[bib]
@article{RISC6774,
author = {Jiayue Qi},
title = {{A tree-based algorithm for the integration of monomials in the Chow ring of the moduli space of stable marked curves of genus zero}},
language = {english},
journal = {Journal of Symbolic Computation},
volume = {122},
number = {102253},
pages = {--},
isbn_issn = {ISSN: 0747-7171},
year = {2024},
refereed = {yes},
length = {52},
url = {https://doi.org/10.1016/j.jsc.2023.102253}
}
[Schneider]

Representation of hypergeometric products of higher nesting depths in difference rings

E.D. Ocansey, C. Schneider

J. Symb. Comput. 120, pp. 1-50. 2024. ISSN: 0747-7171. arXiv:2011.08775 [cs.SC]. [doi]
[bib]
@article{RISC6688,
author = {E.D. Ocansey and C. Schneider},
title = {{Representation of hypergeometric products of higher nesting depths in difference rings}},
language = {english},
journal = {J. Symb. Comput.},
volume = {120},
pages = {1--50},
isbn_issn = {ISSN: 0747-7171},
year = {2024},
note = {arXiv:2011.08775 [cs.SC]},
refereed = {yes},
length = {50},
url = {https://doi.org/10.1016/j.jsc.2023.03.002}
}
[Schneider]

Error bounds for the asymptotic expansion of the partition function

Koustav Banerjee, Peter Paule, Cristian-Silviu Radu, Carsten Schneider

Rocky Mt J Math 54(6), pp. 1551-1592. 2024. ISSN: 357596. arXiv:2209.07887 [math.NT]. [doi] [pdf]
[bib]
@article{RISC6710,
author = {Koustav Banerjee and Peter Paule and Cristian-Silviu Radu and Carsten Schneider},
title = {{Error bounds for the asymptotic expansion of the partition function}},
language = {english},
abstract = {Asymptotic study on the partition function $p(n)$ began with the work of Hardy and Ramanujan. Later Rademacher obtained a convergent series for $p(n)$ and an error bound was given by Lehmer. Despite having this, a full asymptotic expansion for $p(n)$ with an explicit error bound is not known. Recently O'Sullivan studied the asymptotic expansion of $p^{k}(n)$-partitions into $k$th powers, initiated by Wright, and consequently obtained an asymptotic expansion for $p(n)$ along with a concise description of the coefficients involved in the expansion but without any estimation of the error term. Here we consider a detailed and comprehensive analysis on an estimation of the error term obtained by truncating the asymptotic expansion for $p(n)$ at any positive integer $n$. This gives rise to an infinite family of inequalities for $p(n)$ which finally answers to a question proposed by Chen. Our error term estimation predominantly relies on applications of algorithmic methods from symbolic summation. },
journal = {Rocky Mt J Math },
volume = {54},
number = {6},
pages = {1551--1592},
isbn_issn = {ISSN: 357596},
year = {2024},
note = {arXiv:2209.07887 [math.NT]},
refereed = {yes},
keywords = {partition function, asymptotic expansion, error bounds, symbolic summation},
length = {43},
url = {https://www.doi.org/10.1216/rmj.2024.54.1551}
}
[Schneider]

Asymptotics for the reciprocal and shifted quotient of the partition function

Koustav Banerjee, Peter Paule, Cristian-Silviu Radu, Carsten Schneider

Technical report no. 24-06 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). December 2024. Licensed under CC BY 4.0 International. [doi] [pdf]
[bib]
@techreport{RISC7085,
author = {Koustav Banerjee and Peter Paule and Cristian-Silviu Radu and Carsten Schneider},
title = {{Asymptotics for the reciprocal and shifted quotient of the partition function}},
language = {english},
abstract = { Let $p(n)$ denote the partition function. In this paper our main goal is to derive an asymptotic expansion up to order $N$ (for any fixed positive integer $N$) along with estimates for error bounds for the shifted quotient of the partition function, namely $p(n+k)/p(n)$ with $kin mathbb{N}$, which generalizes a result of Gomez, Males, and Rolen. In order to do so, we derive asymptotic expansions with error bounds for the shifted version $p(n+k)$ and the multiplicative inverse $1/p(n)$, which is of independent interest.},
number = {24-06},
year = {2024},
month = {December},
keywords = {{integer partitions, Hardy-Ramanujan Rademacher formula, asymptotic expansion, shifted quotient of partitions, symbolic summation},
length = {43},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Schreiner]

Semantics-Based Rapid Prototyping of a Machine Controller Language

Wolfgang Schreiner, William Steingartner

In: 2024 IEEE 17th International Scientific Conference on Informatics, Poprad, Slovakia, November 13-15, Valerie Novitzká, Anikó Szakál (ed.), pp. 348-353. 2024. IEEE, ISBN 979-8-3503-8767-4.
[bib]
@inproceedings{RISC7063,
author = {Wolfgang Schreiner and William Steingartner},
title = {{Semantics-Based Rapid Prototyping of a Machine Controller Language}},
booktitle = {{2024 IEEE 17th International Scientific Conference on Informatics, Poprad, Slovakia, November 13-15}},
language = {english},
abstract = {We present the use of the semantics-based language generator SLANG to implement a machine controller language EFSM which is based on the principle of extended finite state machines. SLANG allows to rapidly prototype EFSM by a formal definition of the language's abstract syntax, concrete syntax, type system, and denotational semantics; from this, SLANG generates a parser, a printer, a type checker, and an interpreter for EFSM. Subsequently we implement in EFSM a controller for an (idealized) robot vacuum cleaner and validate its operation by simulation and visualization. Our presentation may thus also serve as a template for the semantics-based rapid prototyping of other domain-specific languages.},
pages = {348--353},
publisher = {IEEE},
isbn_issn = {ISBN 979-8-3503-8767-4},
year = {2024},
editor = {Valerie Novitzká and Anikó Szakál},
refereed = {yes},
keywords = {rapid prototyping, semantics of programming languages, interpreters, automata, embedded systems},
sponsor = {Aktion Österreich-Slowakei grants 2023-03-15-001 and 2024-05-15-001, KEGA project 030TUKE-4/2023},
length = {6}
}
[STUDENT]

Highway Node Routing

Christian Huber

Technical report no. 24-08 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). July 2024. Bachelor thesis at RISC, Johannes Kepler University Linz. Licensed under CC BY 4.0 International. [doi] [pdf]
[bib]
@techreport{RISC7088,
author = {Christian Huber},
title = {{Highway Node Routing}},
language = {english},
abstract = {A routing server stands and falls with the routing algorithm behind it. In today’s world,where waiting times are less and less tolerated, it is all the more important to keep theresponse time as short as possible. After all, if the query takes too long, users are more likelyto switch providers than wait for the result. The more queries the system has to process,the more serious the problem becomes. The Dijkstra algorithm quickly comes to mind as asolution. However, this reaches its limits with larger traffic graphs, as we will see later. Amore sophisticated solution is required here: the highway node routing method introducedby D. Schultes. We will look at this approach step by step and check whether it satisfies therequirements of our problem.The idea behind this method is to add a hierarchy to the traffic graph. Each layer is asubset of the lower layers, maintaining the property of the optimal route. During the query,we move step by step to a higher layer, whereby fewer and fewer nodes and edges have to betaken into account, thereby achieving a significant acceleration. This idea emerges from thetraffic network. Assume that all roads are in the lowest layer. The first layer contains stateand federal roads and motorways. The second layer contains federal roads and motorwaysand the last layer contains only motorways. Routing in such a hierarchy no longer providesthe correct result, but it represents the basic idea of the algorithm. In this bachelor thesiswe will look at how we can calculate a correct hierarchy and elaborate the advantages anddisadvantages of this approach.},
number = {24-08},
year = {2024},
month = {July},
note = {Bachelor thesis at RISC, Johannes Kepler University Linz},
keywords = {routing algorithm, Dijkstra algorithm, hierarchy of traffic graphs, },
length = {44},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}
[Windsteiger]

Gray-Box Proving in Theorema

W. Windsteiger

Technical report no. 24-07 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). July 2024. Licensed under CC BY 4.0 International. [doi] [pdf]
[bib]
@techreport{RISC7084,
author = {W. Windsteiger},
title = {{Gray-Box Proving in Theorema}},
language = {english},
abstract = {Many theorems in mathematics have the form of an implication, an equivalence, or an equality, and in the standard prover in the Theorema system such formulas are handled by rewriting. Definitions ofnew function- or predicate symbols are yet another example of formulas that require rewriting in their treatment inthe Theorema system. Both theorems and definitions in practice often carry conditions under which they are valid. Rewriting is, thus, only valid in cases where all side-conditions are met. On the other hand, many of these side-conditions are trivial and when presenting a proof we do not want to distract the reader with lengthy derivations that justify the side-conditions. The goal of this paper is to present the design and implementation of a mechanism that efficiently checks side-conditionsin rewriting while preserving the readability and the explanatory power of a mathematical proof, which has always been of centralinterest in the development of the Theorema system.},
number = {24-07},
year = {2024},
month = {July},
keywords = {Theorema, Automated Theorem Proving, Conditional Rewriting, Mathematica},
length = {8},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}

2023

[Banerjee]

Positivity of the second shifted difference of partitions and overpartitions: a combinatorial approach

Koustav Banerjee

Enumerative Combinatorics and Applications 3, pp. 1-4. 2023. ISSN 2710-2335. [doi]
[bib]
@article{RISC6701,
author = {Koustav Banerjee},
title = {{Positivity of the second shifted difference of partitions and overpartitions: a combinatorial approach}},
language = {english},
journal = {Enumerative Combinatorics and Applications},
volume = {3},
pages = {1--4},
isbn_issn = {ISSN 2710-2335},
year = {2023},
refereed = {yes},
length = {5},
url = {https://doi.org/10.54550/ECA2023V3S2R12}
}
[Banerjee]

Inequalities for the modified Bessel function of first kind of non-negative order

K. Banerjee

Journal of Mathematical Analysis and Applications 524, pp. 1-28. 2023. Elsevier, ISSN 1096-0813. [doi]
[bib]
@article{RISC6700,
author = {K. Banerjee},
title = {{Inequalities for the modified Bessel function of first kind of non-negative order}},
language = {english},
journal = {Journal of Mathematical Analysis and Applications},
volume = {524},
pages = {1--28},
publisher = {Elsevier},
isbn_issn = {ISSN 1096-0813},
year = {2023},
refereed = {yes},
length = {28},
url = {https://doi.org/10.1016/j.jmaa.2023.127082}
}
[Banerjee]

2-Elongated Plane Partitions and Powers of 7: The Localization Method Applied to a Genus 1 Congruence Family

K. Banerjee, N.A. Smoot

Technical report no. 23-10 in RISC Report Series, Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. ISSN 2791-4267 (online). August 2023. Licensed under CC BY 4.0 International. [doi] [pdf]
[bib]
@techreport{RISC6713,
author = {K. Banerjee and N.A. Smoot},
title = {{2-Elongated Plane Partitions and Powers of 7: The Localization Method Applied to a Genus 1 Congruence Family}},
language = {english},
abstract = {Over the last century, a large variety of infinite congruence families have been discovered and studied, exhibiting a great variety with respect to their difficulty. Major complicating factors arise from the topology of the associated modular curve: classical techniques are sufficient when the associated curve has cusp count 2 and genus 0. Recent work has led to new techniques that have proven useful when the associated curve has cusp count greater than 2 and genus 0. We show here that these techniques may be adapted in the case of positive genus. In particular, we examine a congruence family over the 2-elongated plane partition diamond counting function $d_2(n)$ by powers of 7, for which the associated modular curve has cusp count 4 and genus 1. We compare our method with other techniques for proving genus 1 congruence families, and present a second congruence family by powers of 7 which we conjecture, and which may be amenable to similar techniques.},
number = {23-10},
year = {2023},
month = {August},
keywords = {Partition congruences, infinite congruence family, modular functions, plane partitions, partition analysis, modular curve, Riemann surface},
length = {35},
license = {CC BY 4.0 International},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}

Loading…