BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Lambda-Superposition for Successful Hammering - Jasmin Blanchette 
 (Ludwig-Maximilians-Universität München)
DTSTART:20251106T170000Z
DTEND:20251106T180000Z
UID:TALK238813@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:Joint work with Alexander Bentkamp\, Simon Cruanes\, Visa Numm
 elin\, Stephan Schulz\, Sophie Tourret\, Petar Vukmirović\, and Uwe Waldm
 ann\n\nIsabelle's Sledgehammer\, the Lean Hammer\, and other hammers are u
 seful for automatically proving theorems from mathematics and computer sci
 ence. But until a few years ago\, Sledgehammer relied mostly on first-orde
 r automated theorem provers\, which limited its usefulness. In this talk\,
  I will describe my work\, and especially my colleagues' work\, on native 
 higher-order provers that can serve as hammer backends. We developed lambd
 a-superposition\, a proof calculus that generalizes the highly successful 
 superposition calculus implemented by first-order provers such as E\, SPAS
 S\, and Vampire to higher-order logic. This is the logic of HOL4\, HOL Lig
 ht\, and Isabelle/HOL and a fragment of Lean's logic without dependent typ
 es. The calculus is implemented in Duper\, E\, slam\, and Zipperposition. 
 Sledgehammer's success rate has gone up\, and Zipperposition has won troph
 ies at system competitions.\n\n\n=== Online talk ===\n\nJoin Zoom Meeting 
 https://cam-ac-uk.zoom.us/j/89856091954?pwd=Bba77QB2KuTideTlH6PjAmbXLO8HbY
 .1\n\nMeeting ID: 898 5609 1954 Passcode: ITPtalk
LOCATION:Online\; live-streamed at MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR