64 citations · 592 across the 44 of their papers we have counts for
7 papers · 1 filter
Machine-Assisted Proofs (ICM 2018 Panel)
James Davenport, Bjorn Poonen, James Maynard +3
This submission to arXiv is the report of a panel session at the 2018 International Congress of Mathematicians (Rio de Janeiro, August). It is intended that, while v1 is that repor…
Non-linear Real Arithmetic Benchmarks derived from Automated Reasoning in Economics
C. Mulligan, R. Bradford, J. H. Davenport +2
We consider problems originating in economics that may be solved automatically using mathematical software. We present and make freely available a new benchmark set of such problem…
TheoryGuru: A Mathematica Package to apply Quantifier Elimination
C. Mulligan, J. H. Davenport, M. England
We consider the use of Quantifier Elimination (QE) technology for automated reasoning in economics. There is a great body of work considering QE applications in science and enginee…
Quantifier Elimination for Reasoning in Economics
Casey B. Mulligan, Russell Bradford, James H. Davenport +2
We consider the use of Quantifier Elimination (QE) technology for automated reasoning in economics. QE dates back to Tarski's work in the 1940s with software to perform it dating t…
Using Machine Learning to Improve Cylindrical Algebraic Decomposition
Zongyan Huang, Matthew England, David Wilson +2
Cylindrical Algebraic Decomposition (CAD) is a key tool in computational algebraic geometry, best known as a procedure to enable Quantifier Elimination over real-closed fields. How…
Regular cylindrical algebraic decomposition
J. H. Davenport, A. F. Locatelli, G. K. Sankaran
We show that a strong well-based cylindrical algebraic decomposition P of a bounded semi-algebraic set is a regular cell decomposition, in any dimension and independently of the me…
OpenMath and SMT-LIB
James H. Davenport, Matthew England, Roberto Sebastiani +1
OpenMath and SMT-LIB are languages with very different origins, but both "represent mathematics". We describe SMT-LIB for the OpenMath community and consider adaptations for both l…