BEGIN:VCALENDAR
PRODID;X-RICAL-TZSOURCE=TZINFO:-//Calagator//EN
CALSCALE:GREGORIAN
X-WR-CALNAME:Calagator
METHOD:PUBLISH
VERSION:2.0
BEGIN:VTIMEZONE
TZID;X-RICAL-TZSOURCE=TZINFO:America/Los_Angeles
BEGIN:STANDARD
DTSTART:20101107T020000
RDATE:20101107T020000
TZOFFSETFROM:-0700
TZOFFSETTO:-0800
TZNAME:PST
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CREATED;VALUE=DATE-TIME:20110203T190905Z
DTEND;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110207T173000
DTSTART;TZID=America/Los_Angeles;VALUE=DATE-TIME:20110207T163000
DTSTAMP;VALUE=DATE-TIME:20110203T190905Z
LAST-MODIFIED;VALUE=DATE-TIME:20110207T184533Z
UID:http://calagator.org/events/1250459721
DESCRIPTION:Presented by Grant Passmore.
\;\n
\;\nIn automated dedu
ction\, strategy is a vital ingredient in effective proof search. Strate
gy comes in many forms\, but the key is this: user-specifiable adaptatio
ns of general reasoning mechanisms reduce the search space by tailoring
its exploration to a particular class of problems. In fully automatic th
eorem provers\, this may happen through formula weights\, term orders an
d quantifier triggers. In interactive proof assistants\, one may build s
trategies by programming tactics and carefully crafting systems of rewri
te rules. Given that automated deduction often takes place over undecida
ble theories\, the recognition of a need for strategy is natural and hap
pened early in the field. In computer algebra\, the situation is rather
different.
\;\n
\;\nIn computer algebra\, the theories one works o
ver are often decidable but inherently infeasible. For instance\, the th
eory of real closed fields (i.e.\, nonlinear real arithmetic) is decidab
le\, 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 com
es to practical applications\, is an infeasible theory really so differe
nt from an undecidable one?
\;\n
\;\nThe Strategy Challenge in Com
puter Algebra is this: To build theoretical and practical tools allowing
users to exert strategic control over the execution of core computer al
gebra algorithms. In this way\, such algorithms may be tailored to speci
fic 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 dis
sertation: (i) the theory of Abstract Groebner Bases and its use in deve
loping new Groebner basis algorithms tailored to the needs of SMT solver
s (joint with Leo de Moura)\, and (ii) the theory of Abstract Cylindrica
l Algebraic Decomposition and a family of real quantifier elimination al
gorithms tailored to the structure of nonlinear real arithmetic problems
arising in specific formal verification tool-chains. The former forms t
he foundation of nonlinear arithmetic in the SMT solver Z3\, and the lat
ter forms the basis of our tool RAHD (Real Algebra in High Dimensions).\
n\nTags: galois\, tech talk\, formal methods\, algebra\n\nImported from:
http://calagator.org/events/1250459721
URL:http://corp.galois.com/blog/2011/2/3/tech-talk-the-strategy-challenge
-in-computer-algebra.html
SUMMARY:Galois Tech talk: The Strategy Challenge in Computer Algebra
LOCATION:Galois\, Inc: 421 SW 6th Ave. Suite 300\, Portland OR 97204 US
SEQUENCE:2
END:VEVENT
END:VCALENDAR