|
|
![]() |
Some of my papers and related work
| Groebner Basis Construction Algorithms Based on Superposition Loops Joint with Dr. Leonardo de Moura, Microsoft Research and Dr. Paul Jackson, LFCS, Edinburgh. In submission (2010). Abstract: We present novel Groebner basis algorithms based on saturation loops used by modern superposition theorem provers. By combining (i) top-level Groebner basis construction strategies based on the OTTER and DISCOUNT saturation loops, and (ii) sophisticated term indexing techniques derived both from ATP literature and from superfluous S-polynomial criteria in Groebner basis theory, we are able to compute Groebner bases for large, largely linear nonlinear systems of polynomial equations which are beyond the reach of previously available methods. These types of systems are typical of those arising from the use of SMT solvers in reasoning about industrial-strength software artifacts with nonlinear arithmetical components. Proving the correctness of these new Groebner basis procedures is nontrivial, and to do so we utilise the recently introduced theory of Abstract Groebner Bases. We illustrate the practical value of the algorithms through an experimental implementation within the Z3 SMT solver. |
pdf (draft) |
| Superfluous S-polynomials in Strategy-Independent
Groebner Bases Joint with Dr. Leonardo de Moura, Microsoft Research. SYNASC-2009 (11th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing). IEEE Computer Society Conference Publishing Series. © IEEE (2009). Abstract: Using the machinery of proof orders originally introduced by Bachmair and Dershowitz in the context of canonical equational proofs, we give an abstract, strategy-independent presentation of Groebner basis procedures and prove the correctness of two classical criteria for recognising superfluous S-polynomials, Buchberger's criteria 1 and 2, w.r.t. arbitrary fair and correct basis construction strategies. To do so, we develop a general method for proving the strategy-independent correctness of superfluous S-polynomial criteria which seems to be quite powerful. We also derive a new superfluous S-polynomial criterion which is a generalisation of Buchberger-1 and is proved to be correct strategy-independently. Note: Until my Ph.D. thesis is complete, this paper is the best foundational reference for the theory of Abstract (a.k.a. `strategy-independent') Groebner Bases. |
|
| On Locally Minimal
Nullstellensatz Proofs Joint with Dr. Leonardo de Moura, Microsoft Research. SMT-2009 (Satisfiability Modulo Theories; co-located with CADE-22). ACM International Conference Proceedings Series (ISBN 978-1-60558-484-3). © ACM (2009). Abstract: Hilbert's weak Nullstellensatz guarantees the existence of algebraic proof objects certifying the unsatisfiability of systems of polynomial equations not satisfiable over any algebraically closed field. Such proof objects take the form of ideal membership identities and can be found algorithmically using Groebner bases and cofactor-based linear algebra techniques. However, these proof objects may contain redundant information: a proper subset of the equational assumptions used in these proofs may be sufficient to derive the unsatisfiability of the original polynomial system. For using Nullstellensatz techniques in SMT-based decision methods, a minimal proof object is often desired. With this in mind, we introduce a notion of locally minimal Nullstellensatz proofs and give ideal-theoretic algorithms for their construction. |
|
| Universality of Polynomial Positivity and a Variant of Hilbert's 17th Problem Joint with Dr. Leonardo de Moura, Microsoft Research. ADDCT-2009 (Automated Deduction: Decidability, Complexity, Tractability; co-located with CADE-22) in work in progress tract. ADDCT-2009 Proceedings (2009). Abstract: We observe that the decision problem for the existential theory of real closed fields (RCF) is simply reducible to the decision problem for RCF over a connective-free universal language in which the only relation symbol is a strict inequality. In particular, every existential RCF sentence phi can be settled by deciding a proposition of the form ``polynomial p (which is a sum of squares) takes on strictly positive values over the reals,'' with p simply derived from phi. Motivated by this observation, we pose the goal of isolating a syntactic criterion characterising the positive definite (i.e., strictly positive) real polynomials. Such a criterion would be a strictly positive analogue to the fact that every positive semidefinite (i.e., non-negative) real polynomial is a sum of squares of rational functions, as established by Artin's positive solution to Hilbert's 17th Problem. We then prove that every positive definite real polynomial is a ratio of a Real Nullstellensatz witness and a positive definite real polynomial. Finally, we conjecture that every positive definite real polynomial is a product of ratios of Real Nullstellensatz witnesses and examine an interesting ramification of this conjecture. |
|
| Combined Decision Techniques for the Existential Theory of the Reals Joint with Dr. Paul Jackson, LFCS, Edinburgh. Calculemus-2009 (16th Symposium on the Integration of Symbolic Computation and Mechanised Reasoning). Lecture Notes in Artificial Intelligence (LNCS/LNAI 5625). © Springer-Verlag (2009). Abstract: Methods for deciding quantifier-free non-linear arithmetical conjectures over \mathbb{R} are crucial in the formal verification of many real-world systems and in formalised mathematics. While non-linear (rational function) arithmetic over \mathbb{R} is decidable, it is fundamentally infeasible: any general decision method for this problem is worst-case exponential in the dimension (number of variables) of the formula being analysed. This is unfortunate, as many practical applications of real algebraic decision methods require reasoning about high-dimensional conjectures. Despite their inherent infeasibility, a number of different decision methods have been developed, most of which have ``sweet spots'' -- e.g., types of problems for which they perform much better than they do in general. Such ``sweet spots'' can in many cases be heuristically combined to solve problems that are out of reach of the individual decision methods when used in isolation. RAHD (``Real Algebra in High Dimensions'') is a theorem prover that works to combine a collection of real algebraic decision methods in ways that exploit their respective ``sweet-spots.'' We discuss high-level mathematical and design aspects of RAHD and illustrate its use on a number of examples. |
|
| Proving SPARK Verification Conditions with SMT Solvers Joint with Dr. Paul Jackson, LFCS, Edinburgh. In submission (2009-2010). Abstract: We have constructed a tool for using SMT (SAT Modulo Theories) solvers to discharge verification conditions (VCs) from programs written in the SPARK language. The tool can drive any solver supporting the SMT-LIB standard input language and has API interfaces for some solvers. SPARK is a subset of Ada used primarily in high-integrity systems in the aerospace, defence, rail and security industries. Formal verification of SPARK programs is supported by tools produced by the UK company Praxis High Integrity Systems. We report in this paper on our experience in proving SPARK VCs using the popular SMT solvers CVC3, Yices, Z3 and Simplify. We find that the SMT solvers can prove virtually all the VCs that are discharged by Praxis's prover, and sometimes more. Average run-times of the fastest SMT solvers are observed to be roughly 1-2x that of the Praxis prover. Significant work is sometimes needed in translating VCs into a form suitable for input to the SMT solvers. A major part of the paper is devoted to a detailed presentation of the translations we implement. |
pdf (draft) |
| A Survey of Sums of Squares Positivstellensatzen Methods in Real Algebraic Geometry In preparation (2008-2010). Abstract: The discipline of real algebraic geometry centers around the study of subsets of n-dimensional Euclidean space definable by boolean combinations of polynomial equations and inequalities. As such objects, known as semialgebraic sets, arise naturally in virtually all mathematical and natural sciences, the development of sophisticated techniques for their analysis is a well-motivated problem. In this survey, we are interested in a feasible semi-decision method for the following question: Given a semialgebraic set S defined as the collection of satisfying real vectors \vec{r} \in \mathbb{R}^n with respect to some conjunctive system of polynomial equations and inequalities, is S empty? As we will see, through methods deeply rooted in Artin's solution to Hilbert's 17th Problem, Stengle's Positivstellensatzen, Gram matrix constructions for quadratic forms, and a subfield of convex optimization known as semidefinite programming, modern sums of squares techniques as developed by Choi, Lam, Harrison, Parrilo, Powers, Reznick, and W\"ormann offer a promising framework for developing a feasible solution to this important problem. |
|
| Hilbert's Tenth Problem is Solvable over \mathbb{Z} and \mathbb{Q} for Rabinowitsch Zero-dimensional Ideals In preparation (2008-2010). Abstract: Hilbert's Tenth Problem asks for a general algorithm to decide if an integral polynomial p(\vec{x}) \in \mathbb{Z}[\vec{x}] has solutions in the ring of integers. In 1970, the work of Davis, Putnam, Robinson, and Matiyasevich culminated in Matiyasevich's proof that no such algorithm can exist. But the story need not end here. One may relativise Hilbert's Tenth Problem over any computable ring, e.g. to any ring whose arithmetical operations are algorithmic. In this direction, Hilbert's Tenth Problem over \mathbb{Q} remains as an important and difficult open problem at the intersection of arithmetic algebraic geometry, algebraic number theory, and mathematical logic. We give a proof, relying in large part on an exploitation of semialgebraic quantifier elimination, that Hilbert's Tenth Problem over \mathbb{Z}, \mathbb{Q}, and any algebraic number field \mathbb{Q}[\vec{\alpha}] is solvable whenever the ideal induced by the polynomial p(\vec{x}) is Rabinowitsch zero-dimensional over \mathbb{C}. |
|
| Affine Varieties and Classifying Ultrafilters In preparation (2008-2010). Abstract: We show how every affine variety can be associated with a unique ``classifying'' ultrafilter derived from the radical ideal corresponding to the variety. |
|
| Does SAT Exhibit Fractal Behavior? Joint with Dr. Joost Joosten, Institute for Logic, Language and Computation (ILLC), Univ. Amsterdam. ILLC Research Report #PP-2008-41 (2008). Abstract: In this paper we study the structure of the set SAT of all satisfiable propositional logical formulas. In particular we raise the question whether the distribution of SAT within the set A of all propositional formulas exhibits fractal behavior. This answer is of course relative to a metric on A. We show that for one such metric there is strong evidence that the distribution does indeed behave wildly. Next we look at an alternative metric. |
|
| Open Euclidean Relations and Decidable Fragments of the True Existential Theory of the Rational Number Field Abstract of BCTCS-2008 talk appears in the Bulletin of the European Association for Theoretical Computer Science (2008). Abstract: First, we call a continuous map f : \mathbb{R}^n -> \mathbb{R} a ``real-extended rational endomap'' (rcr-map) if {f(q) | q \in \mathbb{Q}^n} \subseteq \mathbb{Q}. Second, we call a binary relation R : \mathbb{R}^2 -> 2 an ``open Euclidean relation'' (oe-relation) if for all rcr-maps f, g : \mathbb{R}^n -> \mathbb{R}, {r \in \mathbb{R}^n | R(f(r), g(r))} is open in \mathbb{R}^n under the Euclidean topology. We have shown that over any first-order language L with relation symbols (R_i)_{i \in I}, function symbols (f_j)_{j \in J}, logical symbols {\exists, \and, \or}, and constant symbols (c_k)_{k \in K}, Th_L(<\mathbb{Q},(f_j)_{j \in J},(R_i)_{i \in I},(c_k)_{k \in K}>) is decidable provided that each c_k denotes a rational number and each R_i (resp. f_j ) denotes an oe-relation (resp. rcr-map) that is first-order definable in the full language of ordered rings. |
|
| A Continuous Relaxation for Proving Discrete ACL2 Theorems over Real Closed Fields Joint with Dr. Paul Jackson, LFCS, Edinburgh. Extended abstract appears in the Proceedings of TTVSI, a Festschrift in Honour of Prof. Mike Gordon FRS, The Royal Society, London, UK (2008). Abstract: The work described involves the use of a decision procedure for real closed fields (RCF) to prove theorems originally formulated with rational-valued variables in the ACL2 theorem prover. From a theoretical perspective, we have isolated an interesting nonlinear fragment of the rational number field that admits a continuous relaxation. From a practical perspective, we have used some recent additions to ACL2 aimed at interfacing with external tools to implement our procedure as a ``trusted clause-processor'' relying upon the QEPCAD-B RCF procedure as a trusted oracle. |
pdf (a) pdf (p) |
| Diophantine Sets and Their Decision Problems Undergraduate Honors Thesis, Department of Mathematics, University of Texas at Austin. Supervised by Prof. Dr. Robert S. Boyer (2007). Abstract: We shall examine the genesis and proof of the Davis-Putnam-Robinson-Matiyasevich negative solution to Hilbert's Tenth Problem, and then proceed to prove a handful of elementary new results on definability and decidability in <\mathbb{N}, *>. |
|
|
Feasible Arithmetical Proof Procedures, S.M.T., and I.B.M. 0-year Ph.D. research proposal, LFCS, University of Edinburgh (2007). Abstract: We are interested in practical proof procedures for theorems with significant number-theoretic content, and the integration of such procedures with modern Satisfiability Modulo Theories (S.M.T.) algorithms and Instance Based Methods (I.B.M.). Of particular interest is automation for proving theorems requiring non-linear arithmetic reasoning, a timely, important problem of current interest to many leaders in the field (see Paulson's ongoing EPSRC grant, Hunt et al., and Avigad-Friedman). We propose a jointly theoretical and practical focus with the following high-level goals: (1) the investigation of logical and computational aspects of decidability for fragments of arithmetic, including meta-theoretic methods for combining decision procedures for both disjoint and intersecting theories, and (2) the development of useful heuristics and semi-decision procedures for undecidable or computationally intractable fragments. For practical theorem proving, we find the recent progress of S.M.T. and I.B.M. algorithms wonderful. We believe they warrant substantial study, and we will endeavor to deliver efficient implementations of our procedural findings within state-of-the-art S.M.T. and I.B.M. systems. |
|
| Formal Verification of Graphical Programs Joint with Dr. Jacob Kornerup, National Instruments Corp. U.S. provisional patent pending (#: 6150-03400, 6150-03401) (2006). | url |
|
Master Class in Mathematical Logic Mathematical Research Institute in the Netherlands Graduated (2007) with a research project titled ``Abstract Properties of Partial Combinatory Algebras'' Fellowship kindly endowed by DIAMANT (Discrete Interactive Algorithmic Mathematics Algebra and Number Theory, Dutch Maths. Cluster) Jointly administered by Departement Wiskunde, Universiteit Utrecht, and Subfaculteit Wiskunde der Katholieke Universiteit Nijmegen
Bachelor of Arts in Mathematics with Honors
Summer (June) 2005 Guest Student |
My start in mathematics and computation began with my involvement in the underground art/demo scene of the
late 80s and early 90s. The scene, centered around the online bulletin board system (BBS), was a haven for artists and coders who wished to be challenged by both the limited artistic
mediums of ANSI and XBiN, as well as the limitations and peculiarities of the x86 architecture when used to drive digital media. Beginning in 1995 under the handle skaboy, and
working my way up towards eventually becoming head-coder for ACiD Productions, I authored numerous software packages for the art/demo scene including the
Infusion Bulletin Board System, the Empathy Image Editor (source code, more info), AvengeView image viewer, AvengePackerPro art-pack
manager, and Impulse Tracker Tosser. I will post links to these applications and their source code as I find them on my old hard-drives and on the internet. I am very happy to hear that
Infusion is still used as the foundation of a handful of BBSs in Europe! (Which is quite surprising, since Infusion, as with many other BBS systems from those days, was negatively impacted
by Y2K dating issues).
The mind-blowingly magical city in which I live
June 21st - 23rd, 2010
I will present a talk (joint with Yuri Gurevich) titled ``Algebraic Descriptive Randomness.''
Royal Holloway, University of London
London, England, UK
November 20th, 2009
I presented a talk (joint with Leo de Moura) titled ``Recent Advances in SAT Modulo Nonlinear Real Arithmetic.''
University of Edinburgh,
Scotland, UK
September 26th - 29th, 2009
I presented a talk (joint with Leo de Moura) titled ``Superfluous
S-polynomials in Strategy-independent Groebner Bases.''
West University, Timisoara, Romania,
RISC Linz, Johannes Kepler University, Austria, and
Research Institute e-Austria Timisoara
Timisoara, Romania
co-located with CADE 2009 (Conference on Autmated Deduction)
August 2nd, 2009
I presented a talk (joint with Leo de Moura) titled ``On Locally
Minimal Nullstellensatz Proofs.''
McGill University
Quebec, Montreal, Canada
co-located with CADE 2009 (Conference on Automated Deduction)
August 2nd, 2009
I presented a talk (joint with Leo de Moura) titled ``Universality of
Polynomial Positivity and a Variant of Hilbert's 17th
Problem.''
McGill University
Quebec, Montreal, Canada
July 7th, 2009
I presented a talk (joint with Paul B. Jackson) titled ``Combined Decision Techniques for the Existential Theory of the
Reals.''
Work appears in the book ``Intelligent Computer Mathematics'' published by Springer-Verlag.
Grand Bend, Ontario, Canada
June 26th, 2009
I presented a talk titled ``Some Results on Nonlinear Arithmetic Helpful to Z3.''
The results covered can be found in two joint papers by Leo de Moura and myself:
Microsoft Research Redmond
Redmond, WA, USA
April 16th, 2009
I presented a talk titled ``A High-level Sketch of the RAHD (`Real Algebra in High Dimensions') Decision Method.''
See here for an abstract of my talk.
Microsoft Research Redmond
Redmond, WA, USA
Nov 27-28th, 2008
I presented two posters (both joint with Paul Jackson):
Microsoft Research Cambridge
Cambridge, England, UK
October 30th, 2008
I presented a talk titled ``RAHD: A Feasible Decision Method for Real Algebra in High Dimensions.''
See here for an abstract of my talk.
SRI International
Menlo Park, CA, USA
August 5-17th, 2008
An Advanced Study Institute of the NATO Science for Peace and Security Programme, and
The Institut für Informätik, Technische Universitat München
Marktoberdorf, Germany
I presented a talk titled ``Decision Methods for the Existential Theory of Real Closed Fields.''
June 27th, 2008
SRI International
Menlo Park, CA, USA
June 9-10th, 2008
SRI International
Menlo Park, CA, USA
April 23rd, 2008 (a post-action shot!)
I presented a talk titled ``A Family of Decidable Nonlinear Fragments of the True Existential Theory of the Rational Number Field.''
Centre for Mathematical Sciences
Department of Pure Mathematics and Mathematical Statistics
University of Cambridge
Cambridge, England, UK
April 7-10th, 2008 (an action shot!)
I presented a talk titled ``Open Euclidean Relations and Decidable Fragments of the True Existential Theory of the Rational Number Field.''
Grey College at Durham University
Banquet at Durham Castle (pretty!)
Durham, England, UK
March 25-26th, 2008
Paul Jackson and I presented a short talk and poster on our joint work titled ``A Continuous Relaxation for Proving
Discrete
ACL2 Theorems over Real Closed Fields.''
The Royal Society
London, England, UK
March 17th, 2008
I presented a talk titled ``Isolating Decidable Nonlinear Fragments of Undecidable Number Theories.''
See here for more information.
Department of Informatics
University of Edinburgh
Edinburgh, Scotland, UK
December 11th, 2007
Department of Mathematics
University of East Anglia
Norwich, England, UK
November 15-16th, 2007
Matt Kaufmann, Jacob Kornerup, and Mark Reitblatt presented a ``Rump Session'' talk on
our joint work centered around using the ACL2 theorem prover to prove properties of
programs written in the graphical parallel dataflow programming language LabVIEW/G.
Jeff Kodosky, the inventor of LabVIEW and founder of our theorem proving project, gave
a Keynote Address on his vision for the future
of our project.
Note: I was sadly not able to be there in person.
Co-located with FMCAD-2007
Austin, TX, USA
October 5th, 2007
I presented a talk titled ``Hilbert's Tenth Problem and Some Weak Relatives.''
See here for an abstract of my talk.
Mathematical Reasoning Group
University of Edinburgh
Edinburgh, Scotland, UK
January 8-12th, 2007
The Lorentz Center
Universeteit Leiden
Leiden, The Netherlands
November 29th - December 2nd, 2006
Center for Mathematical Sciences, and
Computer Laboratory
University of Cambridge
Cambridge, England, UK
October 14-15th, 2006
Institut fur Theoretische Informatik
Technical University of Braunschweig
Braunschweig, Germany
Special Goedel Centennial Meeting
May 17-21st, 2006
Universite du Quebec a Montreal
Montreal, Quebec, Canada
April 7th, 2006
Dr. Jacob Kornerup and I presented a talk titled ``How LabVIEW and its Theorem Prover Help You Build Absolutely Reliable Systems.''
National Instruments Corporation - Main Campus
Austin, TX, USA
April 7th, 2006
I presented my work titled ``Proof Theory in Proof Theory: A Computational Relativisation of Hilbert's Program.''
Under the auspices of the Department of Computer Sciences and the Department of Mathematics
College of Natural Sciences, Welch Hall Forum
University of Texas at Austin
Austin, TX, USA
March 11th-15th, 2006
Special courses in:
Southwestern Center for Arithmetical Algebraic Geometry
University of Arizona
Tucson, AZ, USA
June 8th-12th, 2006 Cancelled
I am on the programme committee. Click here for CfP.
Part of The International Computer Science Symposium in Russia (CSR-2006)
St. Petersburg Department of Steklov Institute of Mathematics, &
Euler International Mathematical Institute
St. Petersburg, Russia
October 19th, 2005 (one day after my 22nd birthday!)
I presented a talk titled "Automated Reasoning in LabVIEW with the Method/ACL2 System."
A short abstract can be found here.
Dept. of Computer Sciences / ACL2 Group
University of Texas, Austin
Austin, TX, USA
August 11-13, 2005
I presented a talk titled "Automated Reasoning in LabVIEW and Some Elementary Thoughts on Proof Theoretic Techniques for Automating Interpretability."
Mathematics and Computer Science Division
Argonne National Laboratory
University of Chicago
Chicago, IL, USA
June 6 - June 17th, 2005
University of Notre Dame
Southbend, IN, USA
Group Photo!
April 2005
IBM Austin Center for Advanced Studies
Austin, TX, USA
March 2005
Stanford University
Palo Alto, CA, USA
May 2004
Carnegie Mellon University
Pittsburgh, PA, USA
Oldschool Underground PC Art/BBS/Demo Scene
I am very happy to report that some of my work in the art-scene is now available as part of the Dark Domain DVD Underground Art Scene Retrospective released by ACiD Productions. This includes source code to many of my applications.
I have also been told that my work in the BBS scene of the late 80s and 90s is part of both the new BBS Documentary
Film (3-part series DVD) and the BBS Historical Library. I think this is very neat -- my sincere thanks go out to those who put
this
together!
Music



The other half of my life is music. With my great friend Barry DeBakey, I am half of the song-writing collective Olney Clark. Our debut self-titled LP (produced by Eddy Hobizal) will be released by the Friendly Police UK label in early 2010 (here is our first music video for the album, `Josefin the writer,' directed and animated by Hanae Seida). Before this, I made a little single/ep, `Let Love Be,' released by Asian Man Records in
October of 2006 (here is a music video for it), and I made a full-length record, `Brokedown Gospel,' which was released in July of 2004 by Asian Man as well, with proceeds benefitting the
Plea For Peace Foundation. See the sweet folks at Asian Man Records for more. (There are also a lot of old releases from projects and bands I was in as a teenager of which I don't have copies anymore; if you do, especially Substandard's `The Complete and Total Unabridged Guide to Life, Happiness, and Humanity,' or The Record Time's `Almost Always,' then please get in touch!)
Memberships
The Edinburgh Mathematical Society
The American Mathematical Society
The Mathematical Association of America
The Association for Symbolic Logic
The Association for Computability in Europe
The Computability and Complexity in Analysis Network
The Association for Automated Reasoning
The Association of Lisp Users
The Association for Advancement of Artificial Intelligence
Foundations of Mathematics Mailing List, NYU et al
The Free Software Foundation (Associate Member)
The Honors Software Development Group
ACL2 Theorem Prover Group
Team CL 2007
(Edinburgh photo by JuanJ on flickr)