Search

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.

In order to design and deploy a feedback controller in a real application, one must determine suitable specifications that the design must meet ("validate"), and then ensure that the chosen specifications have been met ("verify"). In this thesis, we investigate a verification paradigm based on formal methods, such as the Satisfiability Modulo Theories (SMT) and quantifier elimination (Weispfenning's virtual term substitution and quantifier elimination by cylindrical algebraic decomposition) algorithms. Any control design requirement (such as satisfactory performance, robustness to uncertainties, stability, etc.) that can be expressed in a first order logic formula can be (in principle) verified by using one of these methods. Consequently, in principle, this allows us to consider problems like general non-convex optimisation, exact computation of structured singular value, and synthesis of non-convex feasible parameter sets. In practice, the generality of algorithms like quantifier elimination by cylindrical algebraic decomposition come with a downside of high running time when applied to more complex systems with more parameters. This, in some cases, limits the complexity of the system that we could consider. Therefore, we focused our attention on control problems such as obtaining an explicit MPC law for a linear time invariant system with a quadratic objective and polytopic constraints, or computation of the structured singular value for a system under parametric (and not norm-bounded) uncertainty. Such problems can be expressed as quantifier elimination problems with a particular quantification structure that allows us to take advantage of a specialised quantifier elimination algorithm - the quantifier elimination by Weispfenning's virtual term substitution procedure that has much lower worst-case running time on these types of problems than quantifier elimination by cylindrical algebraic decomposition algorithm. Despite these constraints, we were able to apply a quantifier-elimination-based verification framework to clearance of a flight control law developed for a real world industrial system from the aerospace field not only at particular combination of parameters but throughout the whole flight envelope. In conclusion, while in principle formal methods are applicable to a large body of problems arising in control theory, more widespread practical application depends on further research in efficiency and running time improvement in the implementation of these algorithms.

We describe contributions to algorithmic proof techniques for deciding the satisfiability of boolean combinations of many-variable nonlinear polynomial equations and inequalities over the real and complex numbers. In the first half, we present an abstract theory of Grobner basis construction algorithms for algebraically closed fields of characteristic zero and use it to introduce and prove the correctness of Grobner basis methods tailored to the needs of modern satisfiability modulo theories (SMT) solvers. In the process, we use the technique of proof orders to derive a generalisation of S-polynomial superfluousness in terms of transfinite induction along an ordinal parameterised by a monomial order. We use this generalisation to prove the abstract (“strategy-independent”) admissibility of a number of superfluous S-polynomial criteria important for efficient basis construction. Finally, we consider local notions of proof minimality for weak Nullstellensatz proofs and give ideal-theoretic methods for computing complex “unsatisfiable cores” which contribute to efficient SMT solving in the context of nonlinear complex arithmetic. In the second half, we consider the problem of effectively combining a heterogeneous collection of decision techniques for fragments of the existential theory of real closed fields. We propose and investigate a number of novel combined decision methods and implement them in our proof tool RAHD (Real Algebra in High Dimensions). We build a hierarchy of increasingly powerful combined decision methods, culminating in a generalisation of partial cylindrical algebraic decomposition (CAD) which we call Abstract Partial CAD. This generalisation incorporates the use of arbitrary sound but possibly incomplete proof procedures for the existential theory of real closed fields as first-class functional parameters for “short-circuiting” expensive computations during the lifting phase of CAD. Identifying these proof procedure parameters formally with RAHD proof strategies, we implement the method in RAHD for the case of full-dimensional cell decompositions and investigate its efficacy with respect to the Brown-McCallum projection operator. We end with some wishes for the future.

Diagrammatic reasoning (DR) is pervasive in human problem solving as a powerful adjunct to symbolic reasoning based on language-like representations. However, Artificial Intelligence is overwhelmingly based on symbolic representations, with proportionately scant attention to diagrams. This dissertation is a contribution to building artificial agents that can create and use diagrams as part of their problem solving. The work is in a framework in which DR is modeled as a process in which subtasks are solved, as appropriate, either by inference from symbolic representations or by information perceived from a diagram, and subtasks may also act on the diagram, i.e., create or modify objects in the diagram. The perceptions and actions are in fact domain- and task-specific 2D spatial problems defined in terms of properties and relations involving diagrammatic objects. Most DR systems built so far are task-specific, and their developers as a rule have hand-crafted the required perceptions and actions. Our goal is the development of a general, i.e., domain- and task-independent, capability that takes specifications of perceptions and actions and automatically executes them. Thus, this dissertation investigates: 1. A language for a human problem solver to communicate a wide variety of 2D spatial problems relevant to DR, and 2. A general domain-independent framework of underlying representations and reasoning strategies suitable for efficiently solving spatial problems without human intervention. This dissertation will present a high-level language that is extensible, human-usable, and expressive enough to describe a wide variety of spatial problems in terms of constraints. The constraints are specified in first-order logic over the real domain using a vocabulary of objects, properties, relations and actions. Two general and independent strategies – constraint satisfaction and spatial search – are developed for automatically solving the spatial problems specified in that language. Several ideas about how to make these strategies computationally efficient are proposed and illustrated by examples. A traditional AI problem solver is augmented with this spatial problem solver for reasoning with diagrams in different domains for real-world applications. The utility of the framework is judged by the expressiveness of the language, and generality and efficiency of the two strategies.