BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Solving HOL problems using FOL tools - Nik Sultana (University of 
 Cambridge)
DTSTART:20090602T120000Z
DTEND:20090602T130000Z
UID:TALK17990@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:HOL is seen by many as an ideal language for expressing mathem
 atical ideas\, but HOL's expressivity makes its automation more challengin
 g. One frequently finds that HOL problems are "essentially first-order" --
  that is\, \nthey can be faithfully translated into FOL. Automated reasoni
 ng in FOL is quite mature compared to that in HOL. It has been argued that
  for "essentially first-order" \nproblems it is more sensible to carry out
  the translation into FOL and solve using high-performance FOL tools\, rat
 her than attempt to solve the problem using a HOL \nprover. During this ta
 lk I will describe and compare translations from HOL to FOL.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR