BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Inaugural CAIS Lecture - Professor Lawrence Paulson FRS on Automat
 ed Theorem Proving - Professor Lawrence Paulson FRS (Cambridge University)
DTSTART:20230308T183000Z
DTEND:20230308T210000Z
UID:TALK197200@talks.cam.ac.uk
CONTACT:Aaron Turner
DESCRIPTION:* Please note that this is a ticket only event – you must ha
 ve a ticket to attend\n* Full details of the event\, including where to pu
 rchase tickets\, may be found "here":https://www.cambridgeaisocial.org\n\n
 Title: “Automated Theorem Proving: a Technology Roadmap”\n\nAbstract: 
 The technology of automated deduction has a long pedigree. For ordinary fi
 rst-order logic\, the basic techniques had all been invented by 1965: DPLL
  (for large Boolean problems) and the tableau and resolution calculi (for 
 quantifiers). The relationship between automated deduction and AI has been
  complex: does intelligence emerge from deduction\, or is it the other way
  around? Interactive theorem proving further complicates the picture\, wit
 h a human user working in a formal calculus much stronger than first-order
  logic on huge\, open-ended verification problems and needing maximum auto
 mation. Isabelle is an example of a sophisticated interactive prover that 
 also relies heavily on automatic technologies through its nitpick and sled
 gehammer subsystems. The talk will give an architectural overview of Isabe
 lle and its associated tools. The speaker will also speculate on how futur
 e developments\, especially machine learning\, could assist (not replace) 
 the user.\n
LOCATION:Bradfield Centre\, 184 Cambridge Science Park\, Milton Road\, Cam
 bridge\, CB4 0GA
END:VEVENT
END:VCALENDAR