https://arxiv.org/api/Ku20uF5td7uhTu39A7SapYUw0fo 2026-04-09T17:17:39Z 3074 195 15 http://arxiv.org/abs/2507.07889v2 2025-10-31T15:35:28Z

An integro-differential ring is a differential ring that is closed under an integration operation satisfying the fundamental theorem of calculus. Via the Newton--Leibniz formula, a generalized evaluation is defined in terms of integration and differentiation. The induced evaluation is not necessarily multiplicative, which allows to model functions with singularities and leads to generalized shuffle relations. In general, not every element of a differential ring has an antiderivative in the same ring. Starting from a commutative differential ring and a direct decomposition into integrable and non-integrable elements, we construct the free integro-differential ring. This integro-differential closure contains all nested integrals over elements of the original differential ring. We exhibit the relations satisfied by generalized evaluations of products of nested integrals. Investigating these relations of constants, we characterize in terms of Lyndon words certain evaluations of products that determine all others. We also analyze the relation of the free integro-differential ring with the shuffle algebra. To preserve integrals in the original differential ring for computations in its integro-differential closure, we introduce the notion of quasi-integro-differential rings and give two adapted constructions of the integro-differential closure. Finally, in a given integro-differential ring, we consider the internal integro-differential closure of a differential subring and identify it as quotient of the free integro-differential ring by certain constants.

2025-07-10T16:20:13Z 42 pages; minor revision plus new Section 4.2 Clemens G. Raab Georg Regensburger http://arxiv.org/abs/2510.26869v1 2025-10-30T17:49:10Z

Given finitely many consecutive terms of an infinite sequence, we discuss the construction of a polynomial difference equation that the sequence may satisfy. We also present a method to seek a candidate polynomial differential equation for its generating function. It appears that these methods often lead to effective D-algebraic operations.

2025-10-30T17:49:10Z 24 pages. For number theory, see the last section. Comments welcome Bertrand Teguia Tabuguia http://arxiv.org/abs/2510.26429v1 2025-10-30T12:24:37Z

We consider sets/relations/computations defined by *Elementary Inference Systems* I, which are obtained from Smullyan's *elementary formal systems* using Gentzen's notation for inference rules, and proof trees for atoms P(t_1,...,t_n), where predicate P represents the considered set/relation/computation. A first-order theory Th(I), actually a set of definite Horn clauses, is given to I. Properties of objects defined by I are expressed as first-order sentences F, which are proved true or false by *satisfaction* M |= F of F in a *canonical* model M of Th(I). For this reason, we call F a *semantic property* of I. Since canonical models are, in general, incomputable, we show how to (dis)prove semantic properties by satisfiability in an *arbitrary* model A of Th(I). We apply these ideas to the analysis of properties of programming languages and systems whose computations can be described by means of an elementary inference system. In particular, rewriting-based systems.

2025-10-30T12:24:37Z In Proceedings HCVS 2025, arXiv:2510.25468 EPTCS 434, 2025, pp. 10-26 Salvador Lucas Universitat Politecnica de Valencia 10.4204/EPTCS.434.4 http://arxiv.org/abs/2307.02180v5 2025-10-30T09:46:20Z

We introduce a just-in-time runtime program transformation strategy based on repeated recursion unfolding. Our online program optimization generates several versions of a recursion differentiated by the minimal number of recursive steps covered. The base case of the recursion is ignored in our technique. Our method is introduced here on the basis of single linear direct recursive rules. When a recursive call is encountered at runtime, first an unfolder creates specializations of the associated recursive rule on-the-fly and then an interpreter applies these rules to the call. Our approach reduces the number of recursive rule applications to its logarithm at the expense of introducing a logarithmic number of generic unfolded rules. We prove correctness of our online optimization technique and determine its time complexity. For recursions which have enough simplifyable unfoldings, a super-linear is possible, i.e. speedup by more than a constant factor. The necessary simplification is problem-specific and has to be provided at compile-time. In our speedup analysis, we prove a sufficient condition as well as a sufficient and necessary condition for super-linear speedup relating the complexity of the recursive steps of the original rule and the unfolded rules. We have implemented an unfolder and meta-interpreter for runtime repeated recursion unfolding with just five rules in Constraint Handling Rules (CHR) embedded in Prolog. We illustrate the feasibility of our approach with simplifications, time complexity results and benchmarks for some basic tractable algorithms. The simplifications require some insight and were derived manually. The runtime improvement quickly reaches several orders of magnitude, consistent with the super-linear speedup predicted by our theorems.

2023-07-05T10:18:51Z Final version as accepted for Journal Fundamenta Informaticae Fundamenta Informaticae, Volume 194, Issue 3 (October 31, 2025) fi:11547 Thom Fruehwirth 10.46298/fi.11547 http://arxiv.org/abs/2503.11119v2 2025-10-29T05:19:33Z

New results on computing certificates of strictly positive polynomials in Archimedean quadratic modules are presented. The results build upon (i) Averkov's method for generating a strictly positive polynomial for which a membership certificate can be more easily computed than the input polynomial whose certificate is being sought, and (ii) Lasserre's method for generating a certificate by successively approximating a nonnegative polynomial by sums of squares. First, a fully constructive method based on Averkov's result is given by providing details about the parameters; further, his result is extended to work on arbitrary subsets, in particular, the whole Euclidean space $\mathbb{R}^n$, producing globally strictly positive polynomials. Second, Lasserre's method is integrated with the extended Averkov construction to generate certificates. Third, the methods have been implemented and their effectiveness is illustrated. Examples are given on which the existing software package RealCertify appears to struggle, whereas the proposed method succeeds in generating certificates. Several situations are identified where an Archimedean polynomial does not have to be explicitly included in a set of generators of an Archimedean quadratic module. Unlike other approaches for addressing the problem of computing certificates, the methods/approach presented is easier to understand as well as implement.

2025-03-14T06:32:35Z 22 pages, 1 figure Weifeng Shang Jose Abel Castellanos Joo Chenqi Mou Deepak Kapur http://arxiv.org/abs/2505.12085v3 2025-10-26T00:36:34Z

Given a linear equation $\cal E$ of the form $ax + by = cz$ where $a$, $b$, $c$ are positive integers, the $k$-colour Rado number $R_k({\cal E})$ is the smallest positive integer $n$, if it exists, such that every $k$-colouring of the positive integers $\{1, 2, \dotsc, n\}$ contains a monochromatic solution to $\cal E$. In this paper, we consider $k = 3$ and the linear equations $ax + by = bz$ and $ax + ay = bz$. Using SAT solvers, we compute a number of previously unknown Rado numbers corresponding to these equations. We prove new general bounds on Rado numbers inspired by the satisfying assignments discovered by the SAT solver. Our proofs require extensive case-based analyses that are difficult to check for correctness by hand, so we automate checking the correctness of our proofs via an approach which makes use of a new tool we developed with support for operations on symbolically-defined sets -- e.g., unions or intersections of sets of the form $\{f(1), f(2), \dotsc, f(a)\}$ where $a$ is a symbolic variable and $f$ is a function possibly dependent on $a$. No computer algebra system that we are aware of currently has sufficiently capable support for symbolic sets, leading us to develop a tool supporting symbolic sets using the Python symbolic computation library SymPy coupled with the Satisfiability Modulo Theories solver Z3.

2025-05-17T16:59:11Z Appeared at the 10th International Workshop on Satisfiability Checking and Symbolic Computation Tanbir Ahmed Lamina Zaman Curtis Bright http://arxiv.org/abs/2110.10586v4 2025-10-25T01:44:33Z

In this work, we introduce the pattern-domain pilot design paradigm based on a "superposition of orthogonal-building-blocks" with significantly larger contention space to enhance the massive machine-type communications (mMTC) random access (RA) performance in massive multiple-input multiple-output (MIMO) systems.Specifically, the pattern-domain pilot is constructed based on the superposition of $L$ cyclically-shifted Zadoff-Chu (ZC) sequences. The pattern-domain pilots exhibit zero correlation values between non-colliding patterns from the same root and low correlation values between patterns from different roots. The increased contention space, i.e., from N to $\binom{N}{L}$, where $\binom{N}{L}$ denotes the number of all L-combinations of a set N, and low correlation valueslead to a significantly lower pilot collision probability without compromising excessively on channel estimation performance for mMTC RA in massive MIMO systems.We present the framework and analysis of the RA success probability of the pattern-domain based scheme with massive MIMO systems.Numerical results demonstrate that the proposed pattern division random access (PDRA) scheme achieves an appreciable performance gain over the conventional one,while preserving the existing physical layer virtually unchanged. The extension of the "superposition of orthogonal-building-blocks" scheme to "superposition of quasi-orthogonal-building-blocks" is straightforward.

2021-10-20T14:28:53Z Xiaoming Dai Tiantian Yan Qianqian Li Hua Li Xiyuan Wang http://arxiv.org/abs/2510.19787v1 2025-10-22T17:22:09Z

Continuing recent investigations of bounding the tensor rank of matrix multiplication using flip graphs, we present here improved rank bounds for about thirty matrix formats.

2025-10-22T17:22:09Z Manuel Kauers Isaac Wood http://arxiv.org/abs/2510.19383v1 2025-10-22T09:01:03Z

Many systems in our world age, degrade or otherwise move slowly but steadily in a certain direction. When monitoring such systems by means of sensors, one often assumes that some form of `age' is latently present in the data, but perhaps the available sensors do not readily provide this useful information. The task that we study in this paper is to extract potential proxies for this `age' from the available multi-variate time series without having clear data on what `age' actually is. We argue that when we find a sensor, or more likely some discovered function of the available sensors, that is sufficiently monotonic, that function can act as the proxy we are searching for. Using a carefully defined grammar and optimising the resulting equations in terms of monotonicity, defined as the absolute Spearman's Rank Correlation between time and the candidate formula, the proposed approach generates a set of candidate features which are then fitted and assessed on monotonicity. The proposed system is evaluated against an artificially generated dataset and two real-world datasets. In all experiments, we show that the system is able to combine sensors with low individual monotonicity into latent features with high monotonicity. For the real-world dataset of InfraWatch, a structural health monitoring project, we show that two features with individual absolute Spearman's $ρ$ values of $0.13$ and $0.09$ can be combined into a proxy with an absolute Spearman's $ρ$ of $0.95$. This demonstrates that our proposed method can find interpretable equations which can serve as a proxy for the `age' of the system.

2025-10-22T09:01:03Z This preprint has not undergone peer review or any post-submission improvements or corrections. The Version of Record of this contribution is published in Machine Learning and Principles and Practice of Knowledge Discovery in Databases, and is available online at https://doi.org/10.1007/978-3-031-74633-8_2 Guus Toussaint Arno Knobbe 10.1007/978-3-031-74633-8_2 http://arxiv.org/abs/2509.20020v3 2025-10-20T13:29:52Z

In 2011, einsum was introduced to NumPy as a practical and convenient notation for tensor expressions in machine learning, quantum circuit simulation, and other fields. It has since been implemented in additional Python frameworks such as PyTorch and TensorFlow, as well as in other programming languages such as Julia. Despite its practical success, the einsum notation still lacks a solid theoretical basis, and is not unified across the different frameworks, limiting opportunities for formal reasoning and systematic optimization. In this work, we discuss the terminology of tensor expressions and provide a formal definition of the einsum language. Based on this definition, we formalize and prove important equivalence rules for tensor expressions and highlight their relevance in practical applications.

2025-09-24T11:36:02Z 21 pages, 1 figure. Includes formal definitions, proofs of algebraic properties, and nesting/denesting rules for the einsum notation Maurice Wenig Paul G. Rump Mark Blacher Joachim Giesen http://arxiv.org/abs/2510.16944v1 2025-10-19T17:48:29Z

Conceptual modeling has been an important part of constructionist educational practices for many years, particularly in STEM (Science, Technology, Engineering and Mathematics) disciplines. What is not so common is using agent-based simulation to provide students feedback on model quality. This requires the capability of automatically compiling the concept model into its simulation. The VERA (Virtual Experimentation Research Assistant) system is a conceptual modeling tool used since 2016 to provide introductory college biology students with the capability of conceptual modeling and agent-based simulation in the ecological domain. This paper describes VERA and its approach to coupling conceptual modeling and simulation with emphasis on how a model's visual syntax is compiled into code executable on a NetLogo simulation engine. Experience with VERA in introductory biology classes at several universities and through the Smithsonian Institution's Encyclopedia of Life website is related.

2025-10-19T17:48:29Z Spencer Rugaber Scott Bunin Andrew Hornback Sungeun An Ashok Goel http://arxiv.org/abs/2411.14559v2 2025-10-16T12:00:40Z

We show that for any ground term equation systems $E$ and $F$, (1) the union of the generated congruences by $E$ and $F$ is a congruence on the ground term algebra if and only if there exists a ground term equation system $H$ such that the congruence generated by $H$ is equal to the union of the congruences generated by $E$ and $F$ if and only if the congruence generated by the union of $E $ and $F$ is equal to the union of the congruences generated by $E $ and $F$, and (2) it is decidable in square time whether the congruence generated by the union of $E$ and $F$ is equal to the union of the congruences generated by $E $ and $F$, where the size of the input is the number of occurrences of symbols in $E$ plus the number of occurrences of symbols in $F$.

2024-11-21T20:13:10Z 57 pages Sándor Vágvölgyi http://arxiv.org/abs/2505.10246v3 2025-10-16T11:55:10Z

We present an efficient algorithm for computing the leading monomials of a minimal Groebner basis of a generic sequence of homogeneous polynomials. Our approach bypasses costly polynomial reductions by exploiting structural properties conjectured to hold for generic sequences-specifically, that their leading monomial ideals are weakly reverse lexicographic and that their Hilbert series follow a known closed-form expression. The algorithm incrementally constructs the set of leading monomials degree by degree by comparing Hilbert functions of monomial ideals with the expected Hilbert series of the input ideal. To enhance computational efficiency, we introduce several optimization techniques that progressively narrow the search space and reduce the number of divisibility checks required at each step. We also refine the loop termination condition using degree bounds, thereby avoiding unnecessary recomputation of Hilbert series. Experimental results confirm that the proposed method substantially reduces both computation time and memory usage compared to conventional Groebner basis computations for computing the leading monomials of a minimal Groebner basis of generic sequences.

2025-05-15T13:00:44Z Kosuke Sakata Tsuyoshi Takagi http://arxiv.org/abs/2508.19795v2 2025-10-15T12:17:04Z

This paper presents optimizations to improve the scalability of reachability analysis on a subclass of hybrid automata extended with stochasticity. The optimizations target different components of the analysis, such as quantifier elimination for state set projection, and automated parameter selection during the numerical integration. Most importantly, whereas the original method combines forward and backward reachability, we show that the usage of backward reachability is optional for computing maximal reachability probabilities.

2025-08-27T11:21:35Z This paper is accepted for publication (without appendix) in the proceedings of the 27th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC). The appendix was part of the submission and provides additional material which is not included in the SYNASC publication Jonas Stübbe Anne Remke Erika Ábrahám http://arxiv.org/abs/2510.13456v1 2025-10-15T11:59:30Z

A complete reduction $φ$ for derivatives in a differential field is a linear operator on the field over its constant subfield. The reduction enables us to decompose an element $f$ as the sum of a derivative and the remainder $φ(f)$. A direct application of $φ$ is that $f$ is in-field integrable if and only if $φ(f) = 0.$ In this paper, we present a complete reduction for derivatives in a primitive tower algorithmically. Typical examples for primitive towers are differential fields generated by (poly-)logarithmic functions and logarithmic integrals. Using remainders and residues, we provide a necessary and sufficient condition for an element from a primitive tower to have an elementary integral, and discuss how to construct telescopers for non-D-finite functions in some special primitive towers.

2025-10-15T11:59:30Z 10 pages Hao Du Yiman Gao Wenqiao Li Ziming Li