64 citations · 592 across the 44 of their papers we have counts for
45 papers
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…
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…
Proving UNSAT in SMT: The Case of Quantifier Free Non-Linear Real Arithmetic
Erika Abraham, James H. Davenport, Matthew England +1
We discuss the topic of unsatisfiability proofs in SMT, particularly with reference to quantifier free non-linear real arithmetic. We outline how the methods here do not admit triv…
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…
Digital Collections of Examples in Mathematical Sciences
James Harold Davenport
Some aspects of Computer Algebra (notably Computation Group Theory and Computational Number Theory) have some good databases of examples, typically of the form "all the X up to siz…
The DEWCAD Project: Pushing Back the Doubly Exponential Wall of Cylindrical Algebraic Decomposition
R. Bradford, J. H. Davenport, M. England +2
This abstract seeks to introduce the ISSAC community to the DEWCAD project, which is based at Coventry University and the University of Bath, in the United Kingdom. The project see…
Teaching Programming for Mathematical Scientists
Jack Betteridge, Eunice Y. S. Chan, Robert M. Corless +2
Over the past thirty years or so the authors have been teaching various programming for mathematics courses at our respective Universities, as well as incorporating computer algebr…
New Opportunities for the Formal Proof of Computational Real Geometry?
Erika {Á}brahám, James Davenport, Matthew England +2
The purpose of this paper is to explore the question "to what extent could we produce formal, machine-verifiable, proofs in real algebraic geometry?" The question has been asked be…
Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings
Erika Ábrahám, James H. Davenport, Matthew England +1
We present a new algorithm for determining the satisfiability of conjunctions of non-linear polynomial constraints over the reals, which can be used as a theory solver for satisfia…
Formal Methods and CyberSecurity
James H. Davenport
Formal methods have been largely thought of in the context of safety-critical systems, where they have achieved major acceptance. Tens of millions of people trust their lives every…
A UK Case Study on Cybersecurity Education and Accreditation
Tom Crick, James H. Davenport, Alastair Irons +1
This paper presents a national case study-based analysis of the numerous dimensions to cybersecurity education and how they are prioritised, implemented and accredited; from unders…
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…
Identifying the Parametric Occurrence of Multiple Steady States for some Biological Networks
R. Bradford, J. H. Davenport, M. England +8
We consider a problem from biological network analysis of determining regions in a parameter space over which there are multiple steady states for positive real values of variables…
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…
The Potential and Challenges of CAD with Equational Constraints for SC-Square
James H. Davenport, Matthew England
Cylindrical algebraic decomposition (CAD) is a core algorithm within Symbolic Computation, particularly for quantifier elimination over the reals and polynomial systems solving mor…