Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!
Please note the unusual time slot for this talk: it is on Monday, 7 February 2011, at 4:30pm (changed from 1:30pm due to flight delays).
title: The Strategy Challenge in Computer Algebra
presenter: Grant Passmore
time: Monday, 7 February 2011, at 4:30pm (changed from 1:30pm due to flight delays)
location:
Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
abstract:
In automated deduction, strategy is a vital ingredient in effective proof search. Strategy comes in many forms, but the key is this: user-specifiable adaptations of general reasoning mechanisms reduce the search space by tailoring its exploration to a particular class of problems. In fully automatic theorem provers, this may happen through formula weights, term orders and quantifier triggers. In interactive proof assistants, one may build strategies by programming tactics and carefully crafting systems of rewrite rules. Given that automated deduction often takes place over undecidable theories, the recognition of a need for strategy is natural and happened early in the field. In computer algebra, the situation is rather different.
In computer algebra, the theories one works over are often decidable but inherently infeasible. For instance, the theory of real closed fields (i.e., nonlinear real arithmetic) is decidable, but any full quantifier elimination algorithm for it is guaranteed to have worst-case doubly exponential time complexity. The situation is similar with algebraically closed fields (e.g., through Groebner bases), and many others. Usually, decision procedures arising from computer algebra admit little means for a user to control them. But, when it comes to practical applications, is an infeasible theory really so different from an undecidable one?
The Strategy Challenge in Computer Algebra is this: To build theoretical and practical tools allowing users to exert strategic control over the execution of core computer algebra algorithms. In this way, such algorithms may be tailored to specific problem domains. For formal verification efforts, the focus of this challenge upon decision procedures is especially relevant. In this talk, we will motivate this challenge and present two examples from our dissertation: (i) the theory of Abstract Groebner Bases and its use in developing new Groebner basis algorithms tailored to the needs of SMT solvers (joint with Leo de Moura), and (ii) the theory of Abstract Cylindrical Algebraic Decomposition and a family of real quantifier elimination algorithms tailored to the structure of nonlinear real arithmetic problems arising in specific formal verification tool-chains. The former forms the foundation of nonlinear arithmetic in the SMT solver Z3, and the latter forms the basis of our tool RAHD (Real Algebra in High Dimensions).
bio:
Grant Olney Passmore is a Postdoctoral Associate at Clare Hall, University Cambridge and Research Associate at LFCS, University Edinburgh. He works on the joint Cambridge-Edinburgh EPSRC grant “Automatic Proof Procedures for Polynomials and Special Functions” with Larry Paulson (Cambridge) and Paul B. Jackson (Edinburgh), continuing work begun in his Edinburgh PhD dissertation “Combined Decision Procedures for Nonlinear Arithmetics: Real and Complex” (supervised by Paul B. Jackson). He is currently on short leave from the grant as a Visiting Researcher with Yuri Gurevich at Microsoft Research, Redmond.