BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//DTU.dk//NONSGML DTU.dk//EN
CALSCALE:GREGORIAN
BEGIN:VEVENT
DTSTART:20171012T130000
DTEND:20171012T153000
SUMMARY:Proof Assistants and Related Tools, The PART & PART 2 Projects
DESCRIPTION:<p>Workshop 12 October 2017 (Thursday) at DTU Meeting Center building 101 room S04\n</p>\n<ul>\n    <li>13:00-14:00 Andreas Halkj&aelig;r From (DTU Compute): FIT - From's Isabelle Tutorial - Verification of Quicksort\n    </li>\n    <li>14:30-15:30 Uwe Waldmann (Max-Planck-Institut f&uuml;r Informatik - Saarbr&uuml;cken): Saturation Theorem Proving - Basic Ideas, History, and Recent Developments\n    </li>\n</ul>\n<p>\nAbstract 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.\n</p>\n<p>All are welcome. Registration is not necessary. More information is available here: <a href="http://part.compute.dtu.dk/">http://part.compute.dtu.dk/</a>\n</p>\n<p>Organizers:\nMichael Reichhardt Hansen, Anne Elisabeth Haxthausen, Sebastian Alexander M&ouml;dersheim and J&oslash;rgen Villadsen (DTU Compute)\n</p>\n<p>Supported by DTU Compute's Strategic Foundation\n</p>
X-ALT-DESC;FMTTYPE=text/html:<p>Workshop 12 October 2017 (Thursday) at DTU Meeting Center building 101 room S04\n</p>\n<ul>\n    <li>13:00-14:00 Andreas Halkj&aelig;r From (DTU Compute): FIT - From's Isabelle Tutorial - Verification of Quicksort\n    </li>\n    <li>14:30-15:30 Uwe Waldmann (Max-Planck-Institut f&uuml;r Informatik - Saarbr&uuml;cken): Saturation Theorem Proving - Basic Ideas, History, and Recent Developments\n    </li>\n</ul>\n<p>\nAbstract 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.\n</p>\n<p>All are welcome. Registration is not necessary. More information is available here: <a href="http://part.compute.dtu.dk/">http://part.compute.dtu.dk/</a>\n</p>\n<p>Organizers:\nMichael Reichhardt Hansen, Anne Elisabeth Haxthausen, Sebastian Alexander M&ouml;dersheim and J&oslash;rgen Villadsen (DTU Compute)\n</p>\n<p>Supported by DTU Compute's Strategic Foundation\n</p>

URL:https://www.dtu.dk/da/sitecore/Indhold/Institutter/Compute/DTU-Compute-OLD/Forside/Kalender/2017/10/Proof-Assistants-and-Related-Tools
DTSTAMP:20260816T144300Z
UID:{E28FEC84-6E79-415A-87DE-C8F744CCDEFF}-20171012T130000-20171012T130000
LOCATION: DTU Meeting Center building 101 room S04
END:VEVENT
END:VCALENDAR