Workshop 12 October 2017 (Thursday) at DTU Meeting Center building 101 room S04
- 13:00-14:00 Andreas Halkjær From (DTU Compute): FIT - From's Isabelle Tutorial - Verification of Quicksort
- 14:30-15:30 Uwe Waldmann (Max-Planck-Institut für Informatik - Saarbrücken): Saturation Theorem Proving - Basic Ideas, History, and Recent Developments
Abstract for the talk by Uwe Waldmann: With the development of "Hammers", automated theorem provers have become increasingly important for improving the degree of automation of interactive proof systems. Saturation provers, such as E, SPASS, or Vampire, are one of the two categories of automated provers used in this context. These provers are based on variants of the superposition calculus for first-order logic with equality. In this talk, we give an overview of the history of saturation calculi from the 1960's (resolution, completion) to recent developments; we explain how these calculi work, why they work, and what makes them successful in practice.
All are welcome. Registration is not necessary. More information is available here: http://part.compute.dtu.dk/
Organizers:
Michael Reichhardt Hansen, Anne Elisabeth Haxthausen, Sebastian Alexander Mödersheim and Jørgen Villadsen (DTU Compute)
Supported by DTU Compute's Strategic Foundation