BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Progress Report on Leo-II\, an Automatic Theorem Prover for Higher
 -Order Logic - Christoph Benzmueller
DTSTART:20070703T120000Z
DTEND:20070703T130000Z
UID:TALK7417@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:Leo-II is a resolution based theorem prover for classical high
 er-order logic (Church’s simple type theory). We report on the current s
 tage of development of Leo-II. In particular\, we sketch some main aspects
  of Leo-II’s automated proof search procedure\, discuss its cooperation 
 with first-order specialist provers\, and show that Leo-II is also an inte
 ractive proof assistant. We also sketch Leo-II’s shared term data struct
 ure and its term indexing mechanism. Finally\, we present some first perfo
 rmance results.
LOCATION:Computer Laboratory\, William Gates Building\, Room GS15
END:VEVENT
END:VCALENDAR