BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Applying Machine Learning to Heuristic Selection in an Automated T
 heorem Prover - James Bridge (University of Cambridge)
DTSTART:20080513T120000Z
DTEND:20080513T130000Z
UID:TALK11657@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:The speed of finding a proof\, or whether a proof is found at 
 all\, by an automated theorem prover may be critically dependent on the he
 uristic used. A heuristic that works very well in one case may be slow or 
 not work when seeking the proof of a different conjecture. Good heuristics
  are generally found by trial and error and their features are closely tie
 d in with the detailed workings of the theorem prover. If automated theore
 m provers are to be useful to users beyond a small group of specialists th
 e choice of heuristic must be automated.\n\nThe work to be described seeks
  to determine if there is a connection between structural features of the 
 conjecture and axioms and the choice of the best heuristic to be used. Mac
 hine learning is used to find any such connection and embody it in softwar
 e which may be used to automatically select a good heuristic.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR