BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Automatic Proof for Theorems On Transcendental Functions - Lawrenc
 e Paulson (University of Cambridge)
DTSTART:20080205T130000Z
DTEND:20080205T140000Z
UID:TALK9883@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:Speaker: Lawrence Paulson\n\nMany inequalities involving expon
 entials\, logarithms and other functions can be proved automatically by co
 mbining a resolution theorem prover (Metis) with a decision procedure for 
 the theory of real closed fields (QEPCAD). The method should  be applicabl
 e to any functions for which polynomial upper and lower bounds are known. 
 The  \nresolution prover is modified to use the decision procedure to simp
 lify clauses and to detect redundant clauses. The method requires a carefu
 l selection of axioms\, including bounds on the mathematical functions.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR