BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The Strategy Challenge in Computer Algebra - Grant Olney Passmore 
 (University of Cambridge)
DTSTART:20110222T131500Z
DTEND:20110222T141500Z
UID:TALK29837@talks.cam.ac.uk
CONTACT:William Denman
DESCRIPTION:In automated deduction\, strategy is a vital ingredient in eff
 ective proof search. Strategy comes in many forms\, but the key is this: u
 ser-specifiable adaptations of general reasoning mechanisms reduce the sea
 rch space by tailoring its exploration to a particular class of problems. 
 In fully automatic theorem provers\, this may happen through formula weigh
 ts\, term orders and quantifier triggers. In interactive proof assistants\
 , one may build strategies by programming tactics and carefully crafting s
 ystems of rewrite rules. Given that automated deduction often takes place 
 over undecidable theories\, the recognition of a need for strategy is natu
 ral and happened early in the field. In computer algebra\, the situation i
 s rather different.\n\nIn computer algebra\, the theories one works over a
 re 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 wor
 st-case doubly exponential time complexity. The situation is similar with 
 algebraically closed fields (e.g.\, through Groebner bases)\, and many oth
 ers. Usually\, decision procedures arising from computer algebra admit lit
 tle means for a user to control them. But\, when it comes to practical app
 lications\, is an infeasible theory really so different from an undecidabl
 e one?\n\nThe Strategy Challenge in Computer Algebra is this: To build the
 oretical and practical tools allowing users to exert strategic control ove
 r the execution of core computer algebra algorithms. In this way\, such al
 gorithms may be tailored to specific problem domains. For formal verificat
 ion efforts\, the focus of this challenge upon decision procedures is espe
 cially relevant. In this talk\, we will motivate this challenge and presen
 t 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 o
 f Abstract Cylindrical Algebraic Decomposition and a family of real quanti
 fier elimination algorithms tailored to the structure of nonlinear real ar
 ithmetic 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 Di
 mensions).
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR