Presenter: Matthew England
Topic: Quantifier Elimination – a form of simplification in mathematical logic
Date: 15th November 2023
Time: 18:30 for 18:40 lecture start
Location: Webinar – recording available from this link
Synopsis:
Quantifier Elimination (QE) may be considered as a form of simplification in mathematical logic: given a quantified logical statement QE will produce a statement which is equivalent as does not involve the logical quantifiers (there exists / for all). Real QE refers to the case where the logical atoms are constraints on polynomials over the real numbers: in this case the work of Tarski shows that QE is always possible. The first implemented method to achieve this was Cylindrical Algebraic Decomposition (CAD) proposed by Collins. However, CAD is known to have doubly exponential complexity, in effect producing a wall beyond which its application is infeasible. In this talk we will introduce the ideas behind QE and CAD, and describe some recent algorithmic advances which “push back” that doubly exponential wall. We will also discuss some recent applications of this technology to problems emerging in domains as varied as bio-chemistry and economics.
Dr Matthew England is co-Director of the Coventry University Research Centre for Computational Science and Mathematical Modelling. His main research interest is in algorithms for symbolic algebra and symbolic logic, in particular for solving problems with real polynomial systems. His work encompasses the design of new algorithms, their analysis, their integration with other tools, their application, and their optimisation using data science approaches. EP/T015748/1, He currently leads the EPSRC funded DEWCAD Project (Pushing Back the Doubly Exponential Wall of Cylindrical Algebraic Decomposition) and a group of related post-doctoral and PhD students. He previously led projects on the use of machine learning for algorithm optimisation and the integration of computer algebra systems and satisfiability-modulo-theory solvers.