@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{RISC7142,
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-04},
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{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)}
}

@techreport{RISC6750,
author = {K. Banerjee},
title = {{Invariants of the quartic binary form and proofs of Chen's conjectures on inequalities for the partition function and the Andrews' spt function}},
language = {english},
abstract = {An extensive amount of study has been done on inequalities for the partition function, emerged primarily through works of Chen. In particular, the Tur'{a}n inequality and the higher order Tur'{a}n inequalities for $p(n)$ has been one of the most predominant theme. Among many others, one of the most notable one is Griffin, Ono, Rolen, and Zagier's result in which they proved that for every integer $d geq 1$, there exists an integer $N(d)$ such that the Jensen polynomial of degree $d$ and shift $n$ associated with the partition function, denoted by $J^{d,n}_p(x)$, has only distinct real roots for all $n geq N(d)$, earlier conjectured by Chen, Jia, and Wang and Ono independently. Later, Larson and Wagner have provided an estimate of upper bound for $N(d)$. This phenomena in turn implies that the discriminant of $J^{d,n}_p(x)$ is positive; i.e., $text{Disc}_{x}(J^{d,n}_p)>0$. For $d=2$, $text{Disc}_{x}(J^{2,n}_p)>0$ when $n geq N(2)=26$ is equivalent to the fact that $(p(n))_{n geq 26}$ is $log$-concave. In 2017, Chen undertook a comprehensive investigation on inequalities for $p(n)$ through the lens of invariant theory of binary forms of degree $n$. Positivity of the invariant of a quadratic binary form (resp. cubic binary form) associated with $p(n)$ reflects that the sequence $(p(n))_{n geq 26}$ satisfies the Tur'{a}n inequality (resp. $(p(n))_{n geq 95}$ satisfies the higher order Tur'{a}n inequality). Chen further studied on the two invariants for a quartic binary form where its coefficients are shifted values of integer partitions and conjectured four inequalities for $p(n)$. In this paper, we give explicit error bounds for the asymptotic expansion of the shifted partition function $p(n-ell)$ for any non-negative integer $ell$. As an application of these infinite family of inequalities, we confirm the conjectures of Chen. Moreover, three family of inequalities related to the partition function have been studied in this paper, namely, higher order Laguerre inequalities, higher order shifted differences, and higher order log-concavity. In context of higher order Laguerre inequalities for $p(n)$, we settle a conjecture of Wagner. For higher order shifted difference of $p(n)$, we extend a result of Gomez, Males, and Rolen. In context of higher order log-concavity for $p(n)$, we prove discuss on the asymptotic growth for the $r$-fold applications (with $rin {1,2,3}$) of the operator $mathcal{L}$ on $p(n)$ defined by $mathcal{L}(p(n))=p(n)^2-p(n-1)p(n+1)$ and propose a conjecture on infinite log-concavity in this regard. Furthermore, we will show how to construct a unified framework to prove partition function inequalities of the above types and discuss a few possible applications of such construction. Finally, we prove all the Chen's conjectures related to the inequalities for the Andrews' spt function, denoted by spt$(n)$, arising from invariants of quartic binary form using inequalities for the shifted partition function.},
year = {2023},
keywords = {the partition function, Andrews’ spt function, Hardy-Ramanujan-Rademacher for- mula, invariants of binary forms, combinatorial inequalities},
length = {55},
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{RISC6682,
author = {C. Schneider},
title = {{Refined telescoping algorithms in $R\Pi\Sigma$-extensions to reduce the degrees of the denominators}},
language = {english},
abstract = {We present a general framework in the setting of difference ring extensions that enables one to find improved representations of indefinite nested sums such that the arising denominators within the summands have reduced degrees. The underlying (parameterized) telescoping algorithms can be executed in $R\Pi\Sigma$-ring extensions that are built over general $\Pi\Sigma$-fields. An important application of this toolbox is the simplification of d'Alembertian and Liouvillian solutions coming from recurrence relations where the denominators of the arising sums do not factor nicely.},
number = {23-01},
year = {2023},
month = {February},
note = {arXiv:2302.03563 [cs.SC]},
keywords = {telescoping, difference rings, reduced denominators, nested sums},
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{RISC6677,
author = {Diego Dominici and Francisco Marcellan},
title = {{Linear functionals and $Delta$- coherent pairs of the second kind}},
language = {english},
abstract = {We classify all the emph{$Delta$-}coherent pairs of measures of the secondkind on the real line. We obtain $5$ cases, corresponding to all the familiesof discrete semiclassical orthogonal polynomials of class $sleq1.$},
number = {23-02},
year = {2023},
month = {February},
keywords = { Discrete orthogonal polynomials, discrete semiclassical functionals, discrete Sobolev inner products, coherent pairs of discrete measures, coherent pairs of second kind for discrete measures.},
length = {24},
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{RISC6683,
author = {M. Kauers and P. Nuspl and V. Pillwein},
title = {{Order bounds for $C^2$-finite sequences}},
language = {english},
abstract = {A sequence is called $C$-finite if it satisfies a linear recurrence with constant coefficients. We study sequences which satisfy a linear recurrence with $C$-finite coefficients. Recently, it was shown that such $C^2$-finite sequences satisfy similar closure properties as $C$-finite sequences. In particular, they form a difference ring. In this paper we present new techniques for performing these closure properties of $C^2$-finite sequences. These methods also allow us to derive order bounds which were not known before. Additionally, they provide more insight in the effectiveness of these computations. The results are based on the exponent lattice of algebraic numbers. We present an iterative algorithm which can be used to compute bases of such lattices.},
number = {23-03},
year = {2023},
month = {February},
keywords = {Difference equations, holonomic sequences, closure properties, algorithms},
length = {16},
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{RISC6684,
author = {Bruno Buchberger},
title = {{Is ChatGPT Smarter Than Master’s Applicants?}},
language = {English},
abstract = {During the selection procedure for a particular informatics fellowship program sponsored by Upper Austrian companies, I ask the applicants a couple of simple technical questions about programming, etc., in a Zoom meeting. I put the same questions to the dialogue system ChatGPT, [ChatGPT]. The result surprised me: Nearly all answers of ChatGPT were totally correct and nicely explained. Also, in the dialogues to clarify some critical points in the answers, the explanations by ChatGPT were amazingly clear and goal-oriented.In comparison: I tried out the same questions in the personal Zoom interviews with approximately 30 applicants from five countries. Only the top three candidates (with a GPA of 1.0, i.e., the highest possible GPA in their bachelor’s study) performed approximately equally well in the interview. All the others performed (far) worse than ChatGPT. And, of course, all answers from ChatGPT came within 1 to 10 seconds, whereas most of the human applicants' answers needed lengthy and arduous dialogues.I am particularly impressed by the ability of ChatGPT to extract meaningful and well-structured programs from problem specifications in natural language. In this experiment, I also added some questions that ask for proofs for simple statements in natural language, which I do not ask in the student's interviews. The performance of ChatGPT was quite impressive as far as formalization and propositional logic are concerned. In examples where predicate logic reasoning is necessary, the ChatGPT answers are not (yet?) perfect. I am pleased to see that ChatGPT tries to present the proofs in a “natural style” This is something that I had as one of my main goals when I initiated the Theorema project in 1995. I think we already achieved this in the early stage of Theorema, and we performed this slightly better and more systematically than ChatGPT does.I also tried to develop a natural language input facility for Theorema in 2017, i.e., a tool to formalize natural language statements in predicate logic. However, I could not continue this research for a couple of reasons. Now I see that ChatGPT achieved this goal. Thus, I think that the following combination of methods could result in a significant leap forward:- the “natural style” proving methods that we developed within Theorema (for the automated generation of programs from specifications, the automated verification of programs in the frame of knowledge, and the automated proof of theorems in theories), in particular, my “Lazy Thinking Method” for algorithm synthesis from specifications- and the natural language formalization techniques of ChatGPT.I propose this as a research project topic and invite colleagues and students to contact me and join me in this effort: Buchberger.bruno@gmail.com.},
number = {23-04},
year = {2023},
month = {January},
keywords = {ChatGPT, automated programming, program synthesis, automated proving, formalization of natural language, master's screening},
length = {30},
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{RISC6687,
author = {Diego Dominici },
title = {{Recurrence relations for the moments of discrete semiclassical functionals of class $sleq2.$}},
language = {english},
abstract = {We study recurrence relations satisfied by the moments $lambda_{n}left(zright) $ of discrete linear functionals whose first moment satisfies aholonomic differential equation. We consider all cases when the order of theODE is less or equal than $3$.},
number = {23-05},
year = {2023},
month = {March},
keywords = {Discrete orthogonal polynomials, discrete semiclassical functionals, moments.},
length = {81},
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{RISC6706,
author = {Joachim Borya},
title = {{Formalisation of Relational Algebra and a SQL-like Language with the RISCAL Model Checker}},
language = {english},
abstract = {The relational database model is based on the mathematical concept of relational algebra.Query languages have been developed to make data available quickly without creatingdedicated access procedures that depend on the internal representation of the data. SQL(structured query language) can be seen as a quasi-standard for this. This thesis dealswith the formalization and verification of relational algebra and a small but elementarysubset of SQL with the help of the RISCAL model checker, a software tool for the formalspecification and verification of mathematical theories and algorithms.},
number = {23-06},
year = {2023},
month = {May},
keywords = {formal methods, program verification, model checking, automated theorem proving},
length = {77},
type = {Bachelor thesis},
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{RISC6708,
author = {Ágoston Sütő},
title = {{Model Checking Concurrent Systems Under Fairness Constraints in RISCAL}},
language = {english},
abstract = {Model checking is a method for verifying that a program satisfies certain desirable properties formalised using mathematical logic. It is a rigorous method, similar to theorem proving, but it is generally applied when theorem proving would be too difficult due to the complexity of the algorithm, such as in concurrent systems. Model checking is used in the software industry. RISCAL (RISC Algorithm Language) is a language and software system that can be used to describe algorithms over a finite domain, specify their behaviour and then validate the specification. While it mainly focuses on deterministic algorithms, it has limited support for non-deterministic systems as well.The thesis extends the support for non-deterministic systems in RISCAL by allowing the user to specify complex properties about their behaviour in the language of Linear Temporal Logic (LTL) and then to validate them. The core contribution is a model checker implemented in Java using the so-called automaton-based explicit state model checking approach. The software is capable of verifying certain properties that could not be handled by a well-known model checker used in the industry. While in most cases it has underperformed its competitors, our implementation is promising, especially when it comes to properties with certain side conditions, called fairness constraints. The majority of the thesis is be concerned with the theoretical aspects of the automaton-based model checking approach, which is followed by a description of the implementation and various benchmarks.},
number = {23-07},
year = {2023},
month = {May},
keywords = {formal methods, model checking, concurrent systems, nondeterminism, linear temporal logic},
sponsor = {Supported by Aktion Österreich–Slowakei project grant Nr. 2019-10-15-003 “Semantic Modeling of Component-Based Program Systems”},
length = {102},
type = {Master's thesis},
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)}
}