符号计算

For a given ideal I in K[x_1,...,x_n,y_1,...,y_m] in a polynomial ring with n+m variables, we want to find all elements that can be written as f-g for some f in K[x_1,...,x_n] and some g in K[y_1,...,y_m], i.e., all elements of I that…

This paper proposes ideas to speed up the process of creative telescoping, particularly when the telescoper is reducible. One can interpret telescoping as computing an annihilator $L \in D$ for an element $m$ in a $D$-module $M$. The main…

Interactive theorem provers, like Isabelle/HOL, Coq and Lean, have expressive languages that allow the formalization of general mathematical objects and proofs. In this context, an important goal is to reduce the time and effort needed to…

Loop invariants are properties of a program loop that hold before and after each iteration of the loop. They are often employed to verify programs and ensure that algorithms consistently produce correct results during execution.…

We reexamine Smale's alpha theory as a way to certify a numerical solution to an analytic system. For a given point and a system, Smale's alpha theory determines whether Newton's method applied to this point shows the quadratic convergence…

Certification helps to increase trust in formal verification of safety-critical systems which require assurance on their correctness. In hardware model checking, a widely used formal verification technique, phase abstraction is considered…

Solving a system of $m$ multivariate quadratic equations in $n$ variables over finite fields (the MQ problem) is one of the important problems in the theory of computer science. The XL algorithm (XL for short) is a major approach for…

Let $M$ be an $n\times n$ matrix of homogeneous linear forms over a field $\Bbbk$. If the ideal $\mathcal{I}_{n-2}(M)$ generated by minors of size $n-1$ is Cohen-Macaulay, then the Gulliksen-Neg{\aa}rd complex is a free resolution of…

This paper tackles the problem of constructing Bezout matrices for Newton polynomials in a basis-preserving approach that operates directly with the given Newton basis, thus avoiding the need for transformation from Newton basis to monomial…

We present a new methodology for utilising machine learning technology in symbolic computation research. We explain how a well known human-designed heuristic to make the choice of variable ordering in cylindrical algebraic decomposition may…

We introduce hypergeometric-type sequences. They are linear combinations of interlaced hypergeometric sequences (of arbitrary interlacements). We prove that they form a subring of the ring of holonomic sequences. An interesting family of…

Hardware-firmware co-verification is critical to design trustworthy systems. While formal methods can provide verification guarantees, due to the complexity of firmware and hardware, it can lead to state space explosion. There are promising…

A cofactor representation of an ideal element, that is, a representation in terms of the generators, can be considered as a certificate for ideal membership. Such a representation is typically not unique, and some can be a lot more…

In this paper, we examine the structure of systems that are weighted homogeneous for several systems of weights, and how it impacts the computation of Gr\"obner bases. We present several linear algebra algorithms for computing Gr\"obner…

This paper defines a linear representation for nonlinear maps $F:\mathbb{F}^n\rightarrow\mathbb{F}^n$ where $\mathbb{F}$ is a finite field, in terms of matrices over $\mathbb{F}$. This linear representation of the map $F$ associates a…

We investigate the problem of recovering coefficients in scalar nonlinear ordinary differential equations that can be exactly linearized. This contribution builds upon prior work by Lyakhov, Gerdt, and Michels, which focused on obtaining a…

This study proposes the "adaptive flip graph algorithm", which combines adaptive searches with the flip graph algorithm for finding fast and efficient methods for matrix multiplication. The adaptive flip graph algorithm addresses the…

Differential-algebraic equations (DAEs) have been used in modeling various dynamical systems in science and engineering. Several preprocessing methods for DAEs, such as consistent initialization and index reduction, use structural…

We explore algorithmic aspects of a simply transitive commutative group action coming from the class field theory of imaginary hyperelliptic function fields. Namely, the Jacobian of an imaginary hyperelliptic curve defined over $\mathbb…

We solve the so far open problem of constructing all spatial rational curves with rational arc length functions. More precisely, we present three different methods for this construction. The first method adapts a recent approach of (Kalkan…