BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Computer Laboratory Automated Reasoning Group Lunc
hes
SUMMARY:The Strategy Challenge in Computer Algebra - Grant
Olney Passmore (University of Cambridge)
DTSTART;TZID=Europe/London:20110222T131500
DTEND;TZID=Europe/London:20110222T141500
UID:TALK29837AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/29837
DESCRIPTION:In automated deduction\, strategy is a vital ingre
dient in effective proof search. Strategy comes in
many forms\, but the key is this: user-specifiabl
e adaptations of general reasoning mechanisms redu
ce the search space by tailoring its exploration t
o a particular class of problems. In fully automat
ic theorem provers\, this may happen through formu
la weights\, term orders and quantifier triggers.
In interactive proof assistants\, one may build st
rategies by programming tactics and carefully craf
ting systems of rewrite rules. Given that automate
d deduction often takes place over undecidable the
ories\, the recognition of a need for strategy is
natural and happened early in the field. In comput
er algebra\, the situation is rather different.\n\
nIn computer algebra\, the theories one works over
are often decidable but inherently infeasible. Fo
r instance\, the theory of real closed fields (i.e
.\, nonlinear real arithmetic) is decidable\, but
any full quantifier elimination algorithm for it i
s guaranteed to have worst-case doubly exponential
time complexity. The situation is similar with al
gebraically closed fields (e.g.\, through Groebner
bases)\, and many others. Usually\, decision proc
edures arising from computer algebra admit little
means for a user to control them. But\, when it co
mes to practical applications\, is an infeasible t
heory really so different from an undecidable one?
\n\nThe Strategy Challenge in Computer Algebra is
this: To build theoretical and practical tools all
owing users to exert strategic control over the ex
ecution of core computer algebra algorithms. In th
is way\, such algorithms may be tailored to specif
ic problem domains. For formal verification effort
s\, the focus of this challenge upon decision proc
edures is especially relevant. In this talk\, we w
ill motivate this challenge and present two exampl
es from our dissertation: (i) the theory of Abstra
ct Groebner Bases and its use in developing new Gr
oebner basis algorithms tailored to the needs of S
MT solvers (joint with Leo de Moura)\, and (ii) th
e theory of Abstract Cylindrical Algebraic Decompo
sition and a family of real quantifier elimination
algorithms tailored to the structure of nonlinear
real arithmetic problems arising in specific form
al verification tool-chains. The former forms the
foundation of nonlinear arithmetic in the SMT solv
er Z3\, and the latter forms the basis of our tool
RAHD (Real Algebra in High Dimensions).
LOCATION:Computer Laboratory\, William Gates Building\, Roo
m SS03
CONTACT:William Denman
END:VEVENT
END:VCALENDAR