@techreport{RISC7250,
author = {Bruno Buchberger},
title = {{Nakano’s Light Puzzle: A Correctness Proof for a Greedy Algorithm}},
language = {english},
abstract = {We consider Nakano’s Problem: Give a (simple and algorithmic) necessary and sufficient conditionfor a configuration of lights (on/off) in a cube to be transformable to the all-off configuration bycertain touches on the faces of the cube. In this paper, we provide a detailed correctness proof for a“greedy” algorithm for Nakano’s problem. With the same proof technique, we also get anotheralgorithmic criterion for Nakano’s problem, which is based on the notion of “parity of box sums”.We discuss the relevance of such proofs for the recent research on automating mathematicalinvention by a combination of Automated Reasoning techniques and Automated Search of Rele-vant Mathematical Literature through Machine Learning.},
number = {26-05},
year = {2026},
month = {May},
howpublished = {RISC Report},
keywords = {Nakano's problem, light puzzle problem, greedy algorithm, correctness proof, automated mathematical invention, canonical simplification, parity lemma, THEOREMA},
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{RISC7247,
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 variable flavor number scheme to three-loop order}},
language = {english},
abstract = {We describe the variable flavor number scheme to three-loop order, which modifies the massless parton densities by single- and two-mass effects and introduces heavy-quark parton distribution functions for charm and bottom. A renormalization group analysis shows the validity of this picture at large scales $Q^2$, where it resembles the non-power-suppressed heavy-flavor corrections completely. We also provide numerical implementations of a series of charged and neutral current Wilson coefficients.},
number = {26-06},
year = {2026},
month = {July},
note = {DESY 26--064, RISC Report number 26-06, CERN-TH-2026-113, MPP-2026-89, PoS (LL2026) 025},
keywords = {variable flavor number scheme, heavy-quark parton distribution function, computer algebra, numerical implementation},
length = {11},
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{RISC7245,
author = {Besik Dundua and Georg Ehling and Santiago Escobar and Maribel Fernández and Temur Kutsia},
title = {{Quantitative Equational Rewriting}},
language = {english},
abstract = {Rewriting logic is a logical framework for expressing both concurrent computation and logical deduction using equations and re-write rules. Quantitative equational reasoning enriches equations with quantitative measures, expressing concepts such as similarity or proximity rather than mere equality of terms. In this article, we bring these two approaches together and propose a quantitative extension of rewriting logic as a flexible formalism for quantitative deduction and computation.},
number = {26-09},
year = {2026},
month = {June},
keywords = {Quantitative rewriting, quantitative equational reasoning, quantitative matching},
length = {39},
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{RISC7248,
author = {Silvio Ghilardi and Cleo Pau (Editors)},
title = {{Proceedings of the 40th International Workshop on Unification, UNIF 2026}},
language = {english},
abstract = {This volume contains the extended abstract presented at the 40th edition of the annual international workshop on Unification (UNIF 2026), held on July 24th, 2026. The workshop was a part of the Federated Logic Conference (FLoC 2026), that unites the ten leading international conferences focused on mathematical logic and its applications in computer science, as well as over 30 satellite workshops. FLoC 2026 took place in Lisbon.},
number = {26-10},
year = {2026},
month = {July},
keywords = {unification},
length = {80},
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{RISC7242,
author = {C. Schneider},
title = {{A Survey on Symbolic Summation in Difference Rings}},
language = {english},
abstract = {This survey article provides an overview of the fundamental principles used to simplify multi-sums into indefinite nested sums over hypergeometric products in the setting of difference rings. We place special emphasis on the algorithmic translation between hypergeometric sums and the formal difference ring setting. Furthermore, we detail the core summation paradigms of telescoping, creative telescoping, and recurrence solving within difference rings, illustrating these techniques and their underlying algorithms with concrete examples.},
number = {26-07},
year = {2026},
month = {May},
keywords = {Difference ring, telescoping, creative telescoping, parameterized telescoping, recurrence solving.},
length = {31},
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{RISC7257,
author = {J. Bluemlein and A.M. Gavrilik and O. Mykhailiv and C. Schneider},
title = {{The $q$-extension of iterated integrals and nested sums in quantum field theory}},
language = {english},
abstract = {Analytic calculations of zero- and single-scale quantities in perturbative quantum fieldtheory result into special numbers and functions, the first of which have been revealed during the last decades. These are generalizations of the polylogarithm in form of Kummer-Poincar'e iterative integrals over special alphabets and extensions thereof.With growing order in the coupling constant, the polylogarithms, Nielsen integrals, the iterated integrals over linear denominator terms, cyclotomic letters, letters induced by quadratic forms, square-root valued letters, and more general functions contribute. For the nested sums we consider nested harmonic sums, generalized harmonic sums,nested sums implied by quadratic forms, cyclotomic harmonic sums, and nested sumscontaining central binomials. We construct the $q$-extensions of these special functions and of the nested sums, which are associated to them by the series expansion at $x=0$, and their Mellin transform in the $q$-free case. These functions are expected to play a role in perturbative calculations in the case of $q$-deformed commutation relations. For the simpler function spaces closed form solutions are presented. For more involvedalphabets we present the algorithmic steps leading to the $q$-extension for the individual cases. We also derive the determining differential and difference equations of these higher transcendental functions. The $q$-extended special functions arequite different form the corresponding $mu$-extended functions.},
number = {26-11},
year = {2026},
month = {August},
note = {arXiv:2608.02702[math-ph]},
keywords = {q-difference equations, q-differential eqations, q-iterative integrals, q-iterative sums, holonomic closure properties, recurrence solving, quantum field theory},
length = {40},
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{RISC7237,
author = {Wolfgang Schreiner},
title = {{Building a Logical Agent with LangChain ... and Quite Some Vibe Coding}},
language = {english},
abstract = {This document reports on our experience of building an “agentic AI” (Artificial Intelligence) that helps a human to answer logical questions in a trustworthy way. This agent combines a Large Language Model (LLM) (which interacts with the human in natural language) with a logical software (which automatically proves formal theorems). The LLM engages in a dialogue with the human in order to translate their logical question from natural language to a formal proof problem. Once the human is satisfied with the formalization, the LLM invokes the prover to automatically solve the problem and thus answer the question; then the LLM also offers the user the possibility to inspect the successful proof or the unsuccessful proof attempt by calling the prover in an interactive mode. Furthermore, we describe how much of the source code (which is based on on the agent construction framework LangChain) has been “vibe coded”, i.e., itself generated with the help of an LLM.},
number = {26-02},
year = {2026},
month = {March},
keywords = {large language models, automated theorem proving, agentic AI, logical formalization, vibe coding},
length = {73},
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{RISC7239,
author = {Tereso del Río and Wolfgang Schreiner and Martina Seidl and Temur Kutsia and Wolfgang Windsteiger },
title = {{An Intermediate Representation Format for Industrial Optimization Problems - The Translation of OptDSL to MiniZinc}},
language = {english},
abstract = {This report presents the implementation of OptDSL, a Python-inspired domain-specific language for describing optimisation problems. The implementation is based on the translationof a high-level OptDSL formulation of the problem to an intermediate representation in the constraint modelling language MiniZinc, which can be used by multiple state-of-the-art solvers. The report also describes the translation software, illustrates its use on a simplified industrial example, discusses selected implementation details, and suggests directions for further development.},
number = {26-04},
year = {2026},
month = {April},
keywords = {industrial optimization, domain-specific languages, constraint solving, formal languages, translation},
sponsor = {Supported by the FFG project FO999923579 “InProSSA: Industrial Problem Solving Using Symbolic and Subsymbolic AI”},
length = {88},
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)}
}