3 papers
cs.SC2026
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…
cs.SC2024
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,…
cs.SC2024
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…