Inaugural CAIS Lecture - Professor Lawrence Paulson FRS on Automated Theorem Proving

Add to your list(s) Download to your calendar using vCal

• Professor Lawrence Paulson FRS (Cambridge University)
• Wednesday 08 March 2023, 18:30-21:00
• Bradfield Centre, 184 Cambridge Science Park, Milton Road, Cambridge, CB4 0GA.

If you have a question about this talk, please contact Aaron Turner.

• Please note that this is a ticket only event – you must have a ticket to attend
• Full details of the event, including where to purchase tickets, may be found here

Title: “Automated Theorem Proving: a Technology Roadmap”

Abstract: The technology of automated deduction has a long pedigree. For ordinary first-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, with a human user working in a formal calculus much stronger than first-order logic on huge, open-ended verification problems and needing maximum automation. Isabelle is an example of a sophisticated interactive prover that also relies heavily on automatic technologies through its nitpick and sledgehammer subsystems. The talk will give an architectural overview of Isabelle and its associated tools. The speaker will also speculate on how future developments, especially machine learning, could assist (not replace) the user.

This talk is part of the Cambridge AI Social series.

This talk is included in these lists:

• Bradfield Centre, 184 Cambridge Science Park, Milton Road, Cambridge, CB4 0GA
• Cambridge AI Social

Note that ex-directory lists are not shown.