Symbolic Computation
In 2013, Pak and Panova proved the strict unimodality property of $q$-binomial coefficients $\binom{\ell+m}{m}_q$ (as polynomials in $q$) based on the combinatorics of Young tableaux and the semigroup property of Kronecker coefficients.…
There has been an increasing number of applications of machine learning to the field of Computer Algebra in recent years, including to the prominent sub-field of Symbolic Integration. However, machine learning models require an abundance of…
Property Directed Reachability (PDR) is a widely used technique for formal verification of hardware and software systems. This paper presents an incremental version of PDR (IPDR), which enables the automatic verification of system instances…
This paper accompanies a new dataset of non-linear real arithmetic problems for the SMT-LIB benchmark collection. The problems come from an automated proof procedure of Gerhold--Kauers, which is well suited for solution by SMT. The problems…
Cylindrical Algebraic Decomposition (CAD) by projection and lifting requires many iterated univariate resultants. It has been observed that these often factor, but to date this has not been used to optimise implementations of CAD. We…
This paper discusses and evaluates ideas of data balancing and data augmentation in the context of mathematical objects: an important topic for both the symbolic computation and satisfiability checking communities, when they are making use…
Proof terms are syntactic expressions that represent computations in term rewriting. They were introduced by Meseguer and exploited by van Oostrom and de Vrijer to study equivalence of reductions in (left-linear) first-order term rewriting…
In social science, formal and quantitative models, such as ones describing economic growth and collective action, are used to formulate mechanistic explanations, provide predictions, and uncover questions about observed phenomena. Here, we…
We present new algorithms for computing the low $n$ bits or the high $n$ bits of the product of two $n$-bit integers. We show that these problems may be solved in asymptotically 75% of the time required to compute the full $2n$-bit product,…
This paper is concerned with linear algebra based methods for solving exactly polynomial systems through so-called Gr\"obner bases, which allow one to compute modulo the polynomial ideal generated by the input equations. This is a topical…
In this short article I introduce the frab package which provides an alternative interpretation of named vectors in the R programming language; it is available on CRAN. The underlying mathematical object is the free Abelian group.
A new Las Vegas algorithm is presented for the composition of two polynomials modulo a third one, over an arbitrary field. When the degrees of these polynomials are bounded by $n$, the algorithm uses $O(n^{1.43})$ field operations, breaking…
A power series being given as the solution of a linear differential equation with appropriate initial conditions, minimization consists in finding a non-trivial linear differential equation of minimal order having this power series as a…
This paper presents the main features of a system that aims to transform regular expressions into shorter equivalent expressions. The system is also capable of computing other operations useful for simplification, such as checking the…
Narrowing and unification are very useful tools for symbolic analysis of rewrite theories, and thus for any model that can be specified in that way. A very clear example of their application is the field of formal cryptographic protocol…
We consider the problem of answering connectivity queries on a real algebraic curve. The curve is given as the real trace of an algebraic curve, assumed to be in generic position, and being defined by some rational parametrizations. The…
A function is differentially algebraic (or simply D-algebraic) if there is a polynomial relationship between some of its derivatives and the indeterminate variable. Many functions in the sciences, such as Mathieu functions, the Weierstrass…
Recently, symbolic regression (SR) has demonstrated its efficiency for discovering basic governing relations in physical systems. A major impact can be potentially achieved by coupling symbolic regression with asymptotic methodology. The…
One of the few available complete methods for checking the satisfiability of sets of polynomial constraints over the reals is the cylindrical algebraic covering (CAlC) method. In this paper, we propose an extension for this method to…
It is shown how to compute quotients efficiently in non-commutative univariate polynomial rings. This extends earlier work where efficient generic quotients were studied with a primary focus on commutative domains. Fast algorithms are given…