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 Wednesday Seminars
SUMMARY:MetiTarski: An Automatic Theorem Prover for Real-V
alued Special Functions - Larry Paulson - Univ. of
Cambridge Computer Laboratory
DTSTART;TZID=Europe/London:20081126T141500
DTEND;TZID=Europe/London:20081126T151500
UID:TALK13657AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/13657
DESCRIPTION:Logical formulas involving special functions such
as ln\, exp and sin can be proved automatically by
MetiTarski: a resolution theorem prover modified
to call a decision procedure for the theory of rea
l closed fields. (This theory in particular includ
es the real numbers with addition\, subtraction an
d multiplication.) Special functions are approxima
ted by upper and lower bounds\, which are typicall
y ratios of polynomials. The decision procedure s
implifies clauses by deleting literals that are in
consistent with other algebraic facts\; the net ef
fect is to split the problem into numerous cases\,
each covered by a different approximation\, and t
o prove them individually. MetiTarski simplifies a
rithmetic expressions by conversion to a recursive
representation\, followed by flattening of nested
quotients. It can solve many difficult problems f
ound in mathematics reference works\, and it can a
lso solve problems that arise from hybrid and cont
rol systems.\n
LOCATION:Lecture Theatre 1\, Computer Laboratory
CONTACT:Mateja Jamnik
END:VEVENT
END:VCALENDAR