BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:MetiTarski: An Automatic Theorem Prover for Real-Valued Special Fu
 nctions - Larry Paulson - Univ. of Cambridge Computer Laboratory
DTSTART:20081126T141500Z
DTEND:20081126T151500Z
UID:TALK13657@talks.cam.ac.uk
CONTACT:Mateja Jamnik
DESCRIPTION:Logical formulas involving special functions such as ln\, exp 
 and sin can be proved automatically by MetiTarski: a resolution theorem pr
 over modified to call a decision procedure for the theory of real closed f
 ields. (This theory in particular includes the real numbers with addition\
 , subtraction and multiplication.) Special functions are approximated by u
 pper and lower bounds\, which are typically ratios  of polynomials. The de
 cision procedure simplifies clauses by deleting literals that are inconsis
 tent with other algebraic facts\; the net effect is to split the problem i
 nto numerous cases\, each covered by a different approximation\, and to pr
 ove them individually. MetiTarski simplifies arithmetic expressions by con
 version to a recursive representation\, followed by flattening of nested q
 uotients. It can solve many difficult problems found in mathematics refere
 nce works\, and it can also solve problems that arise from hybrid and cont
 rol systems.\n
LOCATION:Lecture Theatre 1\, Computer Laboratory
END:VEVENT
END:VCALENDAR