Show simple item record

dc.contributor.advisorJackson, Paul B.
dc.contributor.authorPassmore, Grant Olney
dc.date.accessioned2012-01-18T10:43:36Z
dc.date.available2012-01-18T10:43:36Z
dc.date.issued2011-11-24
dc.identifier.urihttp://hdl.handle.net/1842/5738
dc.description.abstractWe 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.en
dc.contributor.sponsorEngineering and Physical Sciences Research Council (EPSRC)en
dc.contributor.sponsorUS National Science Foundationen
dc.contributor.sponsorNASAen
dc.contributor.sponsorINRIA/IRISAen
dc.contributor.sponsorDReaM group’s Platform Granten
dc.language.isoenen
dc.publisherThe University of Edinburghen
dc.relation.hasversionLeonardo de Moura and Grant Olney Passmore. On Locally Minimal Nullstellensatz Proofs. In SMT ’09: Proceedings of the 7th International Workshop on Satisfiability Modulo Theories, pages 35–42, New York, NY, USA, 2009. ACM.en
dc.relation.hasversionFlorent Kirchner and Grant Passmore. Thinking Outside the (Arithmetic) Box: Certifying RAHD Computations. In Workshop Proceedings for Logics for System Analysis (short paper), 2010.en
dc.relation.hasversionGrant Olney Passmore and Leonardo de Moura. Superfluous Spolynomials in Strategy-Independent Grobner Bases. Symbolic and Numeric Algorithms for Scientific Computing, International Symposium on, 0:45–53, 2009.en
dc.relation.hasversionGrant Olney Passmore and Leonardo de Moura. Universality of Polynomial Positivity and a Variant of Hilbert’s 17th Problem. In Proceedings of Automated Deduction: Decidability, Complexity, Tractibility (work in progress tract), 2009.en
dc.relation.hasversionGrant Olney Passmore, Leonardo de Moura, and Paul B. Jackson. Grobner Basis Construction Algorithms Based on Theorem Proving Saturation Loops. In Nikolaj Bjorner, Robert Niewenhuis, Helmut Veith, and Andrei Voronkov, editors, Proceedings of Schloss Dagstuhl Seminar on Decision Procedures in Hardware, Software and Bioware, 2010.en
dc.relation.hasversionGrant Olney Passmore and Paul B. Jackson. Combined Decision Techniques for the Existential Theory of the Reals. In Calculemus’09: 16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning, 2009.en
dc.subjectmathematical logicen
dc.subjectquantifier eliminationen
dc.subjectreal closed fieldsen
dc.titleCombined decision procedures for nonlinear arithmetics, real and complexen
dc.typeThesis or Dissertationen
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record