• Home /
  • Webinar: Real Quantifier Elimination: recent algorithmic progress and applications

Join the Coventry branch as they look at Real Quantifier Elimination: recent algorithmic progress and applications.

Watch the video



Quantifier Elimination (QE) may be considered 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.

About the speaker

Matthew England

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.

Our events are for adults aged 16 years and over.

BCS is a membership organisation. If you enjoy this event, please consider joining BCS. You’ll be very welcome. You’ll receive access to many exclusive career development tools, an introduction to a thriving professional community and also help us Make IT Good For Society. Join BCS today

For overseas delegates who wish to attend the event, please note that BCS does not issue invitation letters.

This event is brought to you by: BCS Coventry branch and BCS Leicester branch 

Webinar: Real Quantifier Elimination: recent algorithmic progress and applications
Date and time
Wednesday 15 November, 6:30pm - 9:00pm

This event is sold out