BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Design of a Tableau-Based Automated Theorem Prover and Output of M
 achine-Checkable Proofs
DTSTART:20240223T103000
DTEND:20240223T113000
DTSTAMP:20260916T010535Z
UID:2bbc232b15620e44c9df9fd3a1d0a2fa43ae5870efbdc372a3688a50
CATEGORIES:Conferences - Seminars
DESCRIPTION:By Julie Cailler\, postdoctoral researcher in the University o
 f Regensburg and main author of the Goéland theorem prover\n\nDescripti
 on: Automated deduction is the use of computer programs to automatically p
 rove mathematical theorems. It can be used to detect bugs in critical syst
 ems\, or to help demonstrate mathematical proofs. This talk focuses on the
  presentation of Goéland\, a concurrent tableau-based automated theorem p
 rover\, and the main challenges it faces. These challenges include the imp
 lementation of a fair tableau-based proof search procedure in first-order 
 logic\, the handling of theory reasoning (equality\, set theory\, etc.)\, 
 and the generation of machine-checkable proofs\, i.e.\, proofs that can be
  verified by external tools (Coq\, Lambdapi).\n\nMore information
LOCATION:BC 420 https://plan.epfl.ch/?room==BC%20420 https://epfl.zoom.us/
 j/62454136077
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR