BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Diabelli: a framework for heterogeneous reasoning - Matej Urbas (U
 niversity of Cambridge)
DTSTART:20120508T120000Z
DTEND:20120508T130000Z
UID:TALK37994@talks.cam.ac.uk
CONTACT:William Denman
DESCRIPTION:"Diabelli":https://github.com/urbas/diabelli is the name of ou
 r framework that provides infrastructure for extending\nexisting interacti
 ve theorem provers with heterogeneous reasoning. We use the\nphrase _heter
 ogeneous reasoning_ (or HR)\, to refer to theorem proving\ninvolving both 
 diagrammatic and sentential formulae and proof steps.\n\nI will outline th
 e general idea of HR with concepts such as heterogeneous goals\,\nheteroge
 neous inference steps\, and foreign embedded formulae (or placeholders).\n
 Afterwards\, I will present the Diabelli framework itself\, its architectu
 re\, and\nthe Speedabelle system\, which is an example instantiation of th
 e framework.\nSpeedabelle uses the framework to integrate Isabelle and "Sp
 eedith":https://github.com/urbas/speedith (our\ndiagrammatic reasoner for 
 spider diagrams). This enables heterogeneous\nreasoning with mixed Isabell
 e/HOL formulae and spider diagrams.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR