符号计算

The integration of command-line tools into the Galaxy platform is crucial for making complex computational methods accessible to a broader audience and ensuring reproducible research. However, the manual development of tool wrappers is a…

This paper presents a parallel random-search method for reducing additive complexity in fast matrix multiplication algorithms with ternary coefficients $\{-1,0,1\}$. The approach replaces expensive exact evaluation with fast heuristic…

To check the satisfiability of (non-linear) real arithmetic formulas, modern satisfiability modulo theories (SMT) solving algorithms like NLSAT depend heavily on single cell construction, the task of generalizing a sample point to a…

In differential equation discovery algorithms, numerical differentiation is usually a fixed preliminary step. Current methods improve robustness with data subsampling and sparsity but often ignore the variability from the differentiation…

We develop a general and unconditional framework for certifying the global nonnegativity of multivariate integer polynomials; based on rewriting them as sum of squares modulo their gradient ideals. We remove the two structural assumptions…

Motivated by functional synthesis in sequential circuit construction and quantified boolean formulas (QBF), boolean synthesis serves as one of the core problems in Formal Methods. Recent advances show that decision diagrams (DD) are…

We review the definition and main properties of differential subresultants in order to achieve their implementation in Maple, using the DEtools package. The focus is on computing GCRDs of ordinary differential operators with non necessarily…

Matrix multiplication optimization remains a fundamental challenge in computational mathematics. This work introduces a novel approach that discovers matrix multiplication schemes whose coefficients are restricted to the set $\{-1, 0, 1\}$…

We give explicit low-rank bilinear non-commutative schemes for multiplying structured $n \times n$ matrices with $2 \leq n \leq 5$, which serve as building blocks for recursive algorithms with improved multiplicative factors in asymptotic…

The quest for non-commutative matrix multiplication algorithms in small dimensions has seen a lot of recent improvements recently. In particular, the number of scalar multiplications required to multiply two $4\times4$ matrices was first…

Mahler equations arise in a wide range of contexts including the study of finite automata, regular sequences, algebraic series over Fp(z), and periods of Drinfeld modules. Introduced a century ago by K. Mahler to study the transcendence of…

We present LinApart2, a major update to the LinApart algorithm for univariate partial fraction decomposition. Unlike its predecessor, LinApart2 can handle denominators of arbitrary polynomial degree without explicit factorization, while…

A roadmap for an algebraic set $V$ defined by polynomials with coefficients in the field $\mathbb{Q}$ of rational numbers is an algebraic curve contained in $V$ whose intersection with all connected components of $V\cap\mathbb{R}^{n}$ is…

This paper builds and extends on the authors' previous work related to the algorithmic tool, Cylindrical Algebraic Decomposition (CAD), and one of its core applications, Real Quantifier Elimination (QE). These topics are at the heart of…

Codifying mathematical theories in a proof assistant or computer algebra system is a challenging task, of which the most difficult part is, counterintuitively, structuring definitions. This results in a steep learning curve for new users…

Constraint programming is a general and exact method based on constraint propagation and backtracking search. We provide a function decomposing a constraint network into a ternary constraint network (TCN) with a reduced number of operators.…

This paper deals with simultaneously fast and in-place algorithms for formulae where the result has to be linearly accumulated: some output variables are also input variables, linked by a linear dependency. Fundamental examples include the…

We develop and compare two algorithms for computing first-order right-hand factors in the ring of linear Mahler operators$\ell_r M^r + \dots + \ell_1 M + \ell_0$where $\ell_0, \dots, \ell_r$ are polynomials in~$x$ and $Mx = x^b M$ for some…

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…

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.