64 citations · 592 across the 44 of their papers we have counts for
4 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 Practical Overview of Quantum Computing: Is Exascale Possible?
James H. Davenport, Jessica R. Jones, Matthew Thomason
Despite numerous advances in the field and a seemingly ever-increasing amount of investment, we are still some years away from seeing a production quantum computer in action. Howev…
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…