University of Cambridge > > Cambridge AI Social > Inaugural CAIS Lecture - Professor Lawrence Paulson FRS on Automated Theorem Proving

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

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity