Poly-algorithmic techniques in real quantifier elimination

Quantifier Elimination over the Reals (QE) is a topic in Computer Algebra concerning elimination of quantifiers from boolean formulae of polynomial constraints. QE is known to be worst case doubly exponential time complexity in the number of variables, so optimisation in this area is always of interest. Otherwise, improvements with respect to interface can make usage of QE more tractable. QE problems arise in a range of contexts, notably motion planning (such as robotics), biology, mechanics, and finance. Largely, this work discusses the implementation of a new package QuantifierElimination for the Computer Algebra software Maple. This package, developed in collaboration with Maplesoft, is an amalgamation of contemporary research on two main algorithms for QE, Virtual Term Substitution (VTS) and Cylindrical Algebraic Decomposition (CAD), but a main focus is an investigation into the efficiency & efficacy of a new "poly-algorithm" between these two algorithms. The implementation of CAD includes the first known usage of the Lazard projection for CAD in Maple, and the first known implementation & investigation of new research for equational constraint optimisations with the Lazard projection in CAD. Such equational constraint optimisations may induce mathematical "curtain" occurrences which are ordinarily cause for failure to construct a CAD with frequently desired properties. In conjunction with the first implementation of relevant algorithms from other research, methodology is delineated to ignore, or else attempt to recover from any general failure to construct or evaluate parts of the CAD for QE, including curtains. QuantifierElimination also allows for generation of full CADs without the context of QE, where users can inspect individual cells via various object methods, with the package being largely object oriented where appropriate. Generation of CADs in unquantified contexts has uses in motion planning and real algebraic geometry. Quite often the thesis focuses on finer implementation details & challenges, including with respect to the recent research on equational constraints. Other aims for the package are rich output and "incrementality", to meet the usual aims of implementations of algorithms for QE to be used within Satisfiability Modulo Theory (SMT) solving for the theory of real arithmetic (QF_NRA). Rich output includes production of "witnesses" for fully homogeneously quantified problems, which prove the equivalence of a subset of problems to their quantifier free equivalent. Extension of existing methods enables production of witnesses where the framework of the new polyalgorithm is concerned. The poly-algorithmic methods are extended to be incremental for QE as well. There are a wealth of keyword options and customizable levels of user information to print for users, as the package aims to reconcile with Maple's status as a mathematical toolbox to be easy to use with in depth information being readily available for experienced geometers. Other functions are more pedagogical to accommodate users new to problem formulations in QE and real algebraic geometry. The software is compared via benchmarking against existing QE and CAD software, especially existing packages in Maple, and investigates case studies on examples to demonstrate new methodologies and research.