10 citations · 15 across the 8 of their papers we have counts for
13 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…
A Poly-algorithmic Approach to Quantifier Elimination
James H. Davenport, Zak P. Tonks, Ali K. Uncu
Cylindrical Algebraic Decomposition (CAD) was the first practical means for doing real quantifier elimination (QE), and is still a major method, with many improvements since Collin…
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…
ATLAS: Interactive and Educational Linear Algebra System Containing Non-Standard Methods
Akhilesh Pai, James Harold Davenport
While there are numerous linear algebra teaching tools, they tend to be focused on the basics, and not handle the more advanced aspects. This project aims to fill that gap, focusin…
Cylindrical Algebraic Decomposition with Equational Constraints
Matthew England, Russell Bradford, James H. Davenport
Cylindrical Algebraic Decomposition (CAD) has long been one of the most important algorithms within Symbolic Computation, as a tool to perform quantifier elimination in first order…