61 citations · 693 across the 58 of their papers we have counts for
50 papers · 1 filter
SMT-Solving Induction Proofs of Inequalities
Ali K. Uncu, James H. Davenport, Matthew England
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--Ka…
Iterated Resultants in CAD
James H. Davenport, Matthew England
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…
Data Augmentation for Mathematical Objects
Tereso del Rio, Matthew England
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 sa…
Generating Elementary Integrable Expressions
Rashid Barket, Matthew England, Jürgen Gerhard
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 Integrati…
Explainable AI Insights for Symbolic Computation: A case study on selecting the variable ordering for cylindrical algebraic decomposition
Lynn Pickering, Tereso Del Rio Almajano, Matthew England +1
In recent years there has been increased use of machine learning (ML) techniques within mathematics, including symbolic computation where it may be applied safely to optimise or se…
Levelwise construction of a single cylindrical algebraic cell
Jasper Nalbach, Erika Ábrahám, Philippe Specht +3
Satisfiability Modulo Theories (SMT) solvers check the satisfiability of quantifier-free first-order logic formulas. We consider the theory of non-linear real arithmetic where the…