@techreport{RISC7134,
author = {Ralf Hemmecke and Peter Paule and Cristian-Silviu Radu},
title = {{Computer-assisted construction of Ramanujan-Sato series for 1 over pi}},
language = {english},
abstract = {Referring to ideasof Takeshi Sato, Yifan Yang in~cite{YangDE} described a construction ofseries for $1$ over $pi$ startingwith a pair $(g,h)$, where $g$ is a modular formof weight $2$ and $h$ is a modular function; i.e.,a modular form of weight zero. In this article we present an algorithmicversion,called ``Sato construction''. Series for $1/pi$ obtained this way will becalled ``Ramanujan-Sato''series. Famous series fit into this definition, for instance, Ramanujan'sseries used by Gosperand the series used by the Chudnovsky brothersfor computing millions of digits of $pi$. Weshow that these series are induced by membersof infinite families of Sato triples $(N, gamma_N,tau_N)$ where $N>1$ is an integer and $gamma_N$ a $2times 2$ matrixsatisfying $gamma_N tau_N=N tau_N$ for$tau_N$ being an element from the upper half of thecomplex plane.In addition to procedures for guessingand proving from the holonomic toolbox togetherwiththe algorithm ``ModFormDE'', as describedin~cite{PPSR:ModFormDE1}, a central roleis played by the algorithm ``MultiSamba'',an extension ofSamba (``subalgebra module basis algorithm'') originating fromcite{Radu_RamanujanKolberg_2015} and cite{Hemmecke}.With thehelp of MultiSamba one canfind and prove evaluations of modular functions,at imaginary quadratic points, in terms of nested algebraic expressions.As a consequence,all the series for $1/pi$ constructed withthe help of MultiSamba are proven completelyin a rigorous non-numerical manner.},
number = {25-01},
year = {2025},
month = {January},
keywords = {modular forms and functions, holonomic differential equations, Ramanujan-Sato series for 1 over pi, MultiSamba algorithm},
length = {58},
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)}
}

@techreport{RISC7136,
author = {Wolfgang Schreiner and William Steingartner},
title = {{Semantics-Based Rapid Prototyping of a Subset of SQL}},
language = {english},
abstract = {This report documents the application of our semantics-based language generator SLANG to developing a rapid prototype of a non-trivial domain-specific language, a substantial subset of the Structured Query Language SQL that we have named SubSQL. After developing a mathematical/logical formulation of the language’s abstract syntax, formal type system, and denotational semantics, we have translated this formulation into a SLANG specification from which the SLANG software generates Java code that implements a parser, a printer, a type-checker, and an executor of the language. This implementation is based on several manually created Java classes that implement the mathematical domains and operations used in the formalization, a simple persistent database, and a high-level application programming interface that allows to execute complete SubSQL scripts from file or individual SubSQL commands within Java programs. The results represent a blueprint for the semantics-based development of other domain-specific languages of similar complexity.},
number = {25-02},
year = {2025},
month = {February},
keywords = {formal semantics of programming languages, domain specific languages, rapid prototyping, interpreters},
sponsor = {Aktion Österreich–Slowakei project 2024-05-15-001, KEGA project 030TUKE-4/2023},
length = {179},
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)}
}

@techreport{RISC7141,
author = {Besik Dundua and Temur Kutsia},
title = {{Higher-Order Pattern Unification Modulo Similarity Relations}},
language = {english},
abstract = {The combination of higher-order theories and fuzzy logic can be useful in decision-making tasks that involve reasoning across abstract functions and predicates, where exact matches are often rare or unnecessary. Developing efficient reasoning and computational techniques for such a combined formalism presents a significant challenge. In this paper, we adopt a more straightforward approach aiming at integrating two well-established and computationally well-behaving components: higher-order patterns on one side and fuzzy equivalences expressed through similarity relations based on minimum T-norm on the other. We propose a unification algorithm for higher-order patterns modulo these similarity relations and prove its termination, soundness, and completeness. This unification problem, like its crisp counterpart, is unitary. The algorithm computes the most general unifier with the highest degree of approximation when the given terms are unifiable.},
number = {25-03},
year = {2025},
month = {February},
keywords = {Unification, higher-order patterns, fuzzy similarity relations},
length = {20},
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)}
}

@techreport{RISC7181,
author = {J. Ablinger and A. Behring and J. Blümlein and d and A. De Freitas and A. von Manteuffel and C. Schneider and and K. Schönwald},
title = {{The Single-Mass Variable Flavor Number Scheme at Three-Loop Order}},
language = {english},
abstract = {The matching relations in the unpolarized and polarized variable flavor number scheme at three-loop order are presented in the single-mass case. They describe the process of massive quarks becoming light at large virtualities $Q^2$. In this framework, heavy-quark parton distributions can be defined. Numerical results are presented on the matching relations in the case of the single-mass variable flavor number scheme for the light parton, charm and bottom quark distributions. These relations are process independent. In the polarized case we generally work in the Larin scheme. To two-loop order we present the polarized massive OMEs also in the $overline{rm MS}$ scheme. Fast numerical codes for the single-mass massive operator matrix elements are provided. },
number = {25-04},
year = {2025},
month = {October},
note = {arXiv:2510.02175 [hep-ph]},
keywords = {QCD, Feynman diagrams, computer algebra},
length = {27},
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)}
}

@techreport{RISC7151,
author = {S. Chen and Y. Gao and H. Huang and C. Schneider},
title = {{Telescoping Algorithms for $Sigma^*$-Extensions via Complete Reductions}},
language = {english},
abstract = {A complete reduction on a difference field is a linear operator that enables one to decompose an element of the field as the sum of a summable part and a remainder such thatthe given element is summable if and only if the remainder is equal to zero.In this paper, we present a complete reduction in a tower of $Sigma^*$-extensions that turns to a new efficient framework for the parameterized telescoping problem. Special instances of such $Sigma^*$-extensions cover iterative sums such as the harmonic numbers and generalized versions that arise, e.g., in combinatorics, computer science or particle physics. Moreover, we illustrate how these new ideas can be used to reduce the depth of the given sum and provide structural theorems that connect complete reductions to Karr's Fundamental Theorem of symbolic summation.},
number = {25-05},
year = {2025},
month = {June},
note = {arXiv:2506.08767 [cs.SC]},
keywords = {symbolic summation, difference fields, complete reductions, paramaterized telescoping},
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)}
}

@techreport{RISC7153,
author = {Jack Heseltine},
title = {{Theorema Project: Document Processing}},
language = {english},
abstract = {This work explores the Wolfram Language as a Software Engineering tool, with a particular focus on the Theorema mathematical software package, in combination with the LATEX typesetting system. It delves into the advanced functionalities and paradigms of Wolfram Language, including high-level programming, functional programming, and pattern matching, to showcase these capabilities beyond object oriented programming languages in particular, as applied to mathematical document transformation. Through Theorema, package development using Wolfram Language is demonstrated from conception through execution to the point that the new package can be easily integrated with the existing Theorema system: the associated analysis touches on the workings of Theorema but the focus is on an implementational bridge between computational mathematics and document preparation, aiming to provide easy extensibility and delivering on further Software Engineering principles to make for a rounded Wolfram Language and Theorema package, as the final project output.The thesis also addresses the challenges and methodologies associated with the LATEX typesetting of mathematical content, emphasizing the transformation of Wolfram Language/Theorema notebooks using a Wolfram-Language-native approach. This includes an examination of first-order predicate logic symbols, to ensure coverage at the output side, and the role of (mathematical) expressions in Wolfram Language, the input side, showcasing back-and-forth between typesetting and (symbolic) computational languages, and particularly, recursive parsing of entire notebook expressions as the basic working principle in this approach.},
number = {25-06},
year = {2025},
month = {March 02},
note = {Bachelor Thesis at University of Applied Sciences Hagenberg, bachelor program Software Engineering},
keywords = {Theorema, LaTeX},
length = {76},
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)}
}

@techreport{RISC7182,
author = {J. Ablinger and J. Bluemlein and A. De Freitas and A. von Manteuffel and C. Schneider and Kay Schoenwald},
title = {{The two-mass contributions to the three-loop massive operator matrix elements $tilde{A}_{Qg}^{(3)}$ and $Delta tilde{A}_{Qg}^{(3)}$}},
language = {english},
abstract = {We calculate the two-mass three-loop contributions to the unpolarized and polarized massive operator matrix elements $tilde{A}_{Qg}^{(3)}$ and $Delta tilde{A}_{Qg}^{(3)}$ in $x$-space for a general mass ratio by using a semi-analytic approach. We also compute Mellin moments up to $N = 2000 (3000)$ by an independent method, to which we compare the results in $x$-space. In the polarized case, we work in the Larin scheme. We present numerical results. The two-mass contributions amount to about $50 %$ of the full textcolor{blue}{$O(T_F^2)$} and textcolor{blue}{$O(T_F^3)$} terms contributing to the operator matrix elements. The present result completes the calculation of all unpolarized and polarized massive three-loop operator matrix elements.},
number = {25-07},
year = {2025},
month = {November},
keywords = {operator matrix elements,3-loop massive Feynman diagrams, two masses, symbolic computation},
length = {50},
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)}
}

@techreport{RISC7178,
author = {J. Ablinger and A. Behring and J. Blümlein and A. De Freitas and A. von Manteuffel and C. Schneider and K. Schönwald},
title = {{The three-loop single-mass heavy-flavor corrections to the structure functions $F_2(x,Q^2)$ and $g_1(x,Q^2)$}},
language = {english},
abstract = {We report quantitative results on the single-mass heavy-flavor contributions up to three-loop order to the unpolarized structure function $F_2(x,Q^2)$ and the polarized structure function $g_1(x,Q^2)$ for the first time. These results are relevant for precision QCD analyses of the World deep-inelastic data and the data taken at future colliders, such as the Electron--Ion Collider, in order to measure the strong coupling constant $alpha_s(M_Z^2)$, and the twist-2 parton distribution functions consistently at next-to-next-to-leading order.},
number = {25-08},
year = {2025},
month = {September},
keywords = {single-mass heavy-flavor contributions, QCD, Feynman diagrams, computer algebra},
length = {6},
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)}
}

@techreport{RISC7197,
author = {Ralf Hemmecke and Peter Paule and Cristian-Silviu Radu},
title = {{An Algorithm to Compute Algebraic Relations Between Modular Functions}},
language = {english},
abstract = {The existence of an algebraic relation between two modular functions,in short: a modular equation, is implied by a classical fact from thetheory of compact Riemann surfaces. In this article, we present a new,purely algebraic proof of the existence of modular equations. Oursetting consists of an algorithmic framework which is based on areduction procedure for tuples of formal Laurent series. The resultingalgorithm MultiSamba (“sub-algebra module basis algorithm”) is part ofHemmecke's computer algebra package QEta which has been implemented inFriCAS, a general purpose computer algebra system which is freelyavailable as open source. QEta is a powerful tool-box for actualcomputations. For example, MultiSamba has been used forcomputer-assisted discovery and proofs of Ramanujan-Sato series. Inthis article, we describe the mathematics underlying the MultiSambaalgorithm. Moreover, we explain in detail how MultiSamba works for thederivationof a well-known modular equation betweenthe modular $\lambda$-function and the Klein $j$function.Other examples of the automatic discovery and proving of modularequations include identities by Alladi and others, which suggestrelations of Ramanujan-G\"ollnitz-Gordon type as another promisingarea of MultiSamba application.},
number = {25-09},
year = {2025},
month = {November},
keywords = {modular functions, multisamba, modular equations},
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)}
}

@techreport{RISC7210,
author = {A. Behring and J. Bluemlein and A. De Freitas and A. von Manteuffel and C. Schneider and K. Schoenwald},
title = {{The heavy quark-antiquark asymmetry in the variable flavor number scheme}},
language = {english},
abstract = {The twist-2 heavy-quark and antiquark distributions, as defined in the variable flavor number scheme, turn out to be different due to QCD corrections from three-loop onward. This is caused by terms containing the color factor $d_{abc} d^{abc}$ in the heavy-flavor massive pure-singlet operator matrix elements (OMEs) $A^{rm PS, s, (3)}_{Qq}$ for odd moments in the unpolarized case and for $Delta A^{rm PS, s, (3)}_{Qq}$ for even moments in the polarized case. The dependence on the factorization scale of the OMEs is ruled by the anomalous dimensions $gamma^{rm NS, s, (2)}_{qq}$ and $Delta gamma^{rm NS, s, (2)}_{qq}$. The polarized calculations are performed in the Larin scheme. We compute the corresponding three-loop heavy-flavor distributions $(Delta) f_Q(x,Q^2) - (Delta) f_{overline{Q}}(x,Q^2)$. Compared to the sum of the heavy-quark and antiquark parton distributions, their difference is small, however, non-vanishing. },
number = {25-10},
year = {2025},
month = {December},
note = {arXiv:2512.13508 [hep-ph]},
keywords = {particle physics, QCD, massive 3-loop eynman integrals, computer algebra, solving recurrences},
length = {17},
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)}
}

@techreport{RISC7221,
author = {Viktoria Langenreither},
title = {{A Saturation-Based Automated Theorem Prover for RISCAL}},
language = {english},
abstract = {The aim of this thesis is to integrate a automated theorem prover for first-order logic with equality in the RISC theorem proving (RISCTP) software. The software currently already provides a built-in first-order prover. The MESON prover (model-elimination, subgoaloriented) follows a goal oriented approach. The idea is to provide a different procedure (knowledge-based) to further extend the functionality of RISCTP, since different prove designs lead to a fast proof search for different examples. One way to achieve this is by using the saturation principle, i. e. the prover generates from a set of first-order clauses in a systematic way all logical consequences until a refutation (empty clause) is found.In this thesis we give a throughout theoretical representation of different techniques for first-order provers, based on a comprehensive literature research. In accordance to this, we developed the design of our prover. As most state of the art provers, it is based of the give-clause-algorithm using the DISCOUNT loop to organize the proof search. The inference system is based on a variation of the superposition calculus, using the so-called pure superposition for the equality reasoning (all literals represent equalities). To further extend this prover an interface to an external SMT solver is integrated as well as axioms encoding the special theories of integers and arrays. The implementation of this prover is done as an extension of the RISCTP software using the Java programming language. To evaluate the prover, we used examples that were already defined for evaluating the MESON prover.},
number = {25-11},
year = {2025},
month = {December},
keywords = {automated reasoning, formal methods, program verification},
length = {108},
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)}
}

@techreport{RISC7224,
author = {Tereso del Rio and Wolfgang Schreiner and Martina Seidl and Temur Kutsia and Wolfgang Windsteiger},
title = {{A DSL for Specifying a Class of Industrial Optimisation Problems}},
language = {english},
abstract = {This report documents a newdomain-specific language (DSL) designed to express industrial optimisation problems in a Pythonic and procedural way. This language allows users to describe optimisation models using familiar programming tools such as variables, loops, and conditional statements, instead of low-level mathematical formulations.},
number = {25-12},
year = {2025},
month = {December},
keywords = {industrial optimization, constraint solving, domain-specific languages},
sponsor = {Supported by FFG project 59218671 “InProSSA: Industrial Problem Solving Using Symbolic and Subsymbolic AI”},
length = {19},
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)}
}

@techreport{RISC6894,
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.},
number = {24-01},
year = {2024},
month = {January},
note = {arXiv:2401.16314 [cs.SC]},
keywords = {creative telescoping; symbolic summation, hypergeometric multi-sums, contiguous relations, parameterized recurrences, rational solutions},
length = {26},
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)}
}

@techreport{RISC7042,
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.},
number = {24-02},
year = {2024},
month = {March},
note = {arXiv:2403.00513 [[hep-ph]},
keywords = {Feynman diagram, massive operator matrix elements, computer algebra, differential equations, difference equations, coupled systems, numerics},
length = {14},
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)}
}

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

@techreport{RISC7059,
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}},
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.},
number = {24-04},
year = {2024},
month = {July},
note = {arXiv:2407.02006 [hep-ph]},
keywords = {Feynman integrals, deep-inelastic scattering, numerical results},
length = {12},
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)}
}

@techreport{RISC7062,
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}},
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.},
number = {24-05},
year = {2024},
month = {August},
note = { arXiv:2408.07046 [hep-ph]},
keywords = {Form factor; computer algebra, coupled systems, differential equations, recurrences, analytic continuation, holonomic functions},
length = {18},
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)}
}

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

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

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