BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Rough-and-ready proof reconstruction - Nik Sultana
DTSTART:20110301T131500Z
DTEND:20110301T141500Z
UID:TALK29333@talks.cam.ac.uk
CONTACT:William Denman
DESCRIPTION:This talk addresses the following question: "if we have a proo
 f in one system\, how do we check it using a different system?" . The moti
 vations for asking this question are twofold: one might wish to move proof
 s of propositions between different systems\; one might also wish to use a
  'safer' system to check a proof\, in the spirit of de Bruijn. During the 
 talk I will describe an approach to proof reconstruction which relies on t
 he existing internal automation of Isabelle/HOL to check proofs produced b
 y Leo-II. This is made possible by Isabelle/HOL's good level of automation
 . I will discuss some experimental results which suggest a measure of the 
 strength of Isabelle/HOL's internal automation relative to Leo-II.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR