21 citations · 24 across the 13 of their papers we have counts for
Showing 2023Show all
2 papers · 1 filter
cs.SC2023
Iterated Resultants and Rational Functions in Real Quantifier Elimination
James H. Davenport, Matthew England, Scott McCallum +1
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 Quant…
cs.SC2023
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…