25 citations · 25 across the 4 of their papers we have counts for
4 papers
Enhanced CAD-Based Quantifier Elimination With Multiple Equational Constraints
James H. Davenport, Matthew England, Scott McCallum
This paper presents two enhancements to cylindrical algebraic decomposition (CAD) based quantifier elimination (QE) for cases in which multiple equational constraints are present i…
Towards Verified Polynomial Factorisation
James H. Davenport
Computer algebra systems are really good at factoring polynomials, i.e. writing f as a product of irreducible factors. It is relatively easy to verify that we have a factorisation,…
First steps towards Computational Polynomials in Lean
James Harold Davenport
The proof assistant Lean has support for abstract polynomials, but this is not necessarily the same as support for computations with polynomials. Lean is also a functional programm…
Using the Regular Chains Library to build cylindrical algebraic decompositions by projecting and lifting
Matthew England, David Wilson, Russell Bradford +1
Cylindrical algebraic decomposition (CAD) is an important tool, both for quantifier elimination over the reals and a range of other applications. Traditionally, a CAD is built thro…