Presented by Grant Passmore.

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).