CAIS Lecture (AI + pizza) - Professor Lawrence Paulson FRS

Brought to you by The Artificial Intelligence Group

What do advanced AI systems need in order to be able to think rationally? Not just give the impression that they are doing so (to a lay and impressionable observer), but for real…?

Registration for this event is now closed.

About the event

With the November 2022 release of OpenAI’s ChatGPT, the rate of advance in AI has seemingly gone from meteoric to meteoric on steroids. But many commentators have expressed doubts that Large Language Models such as ChatGPT are truly intelligent.

What do advanced AI systems need in order to be able to think rationally? Not just give the impression that they are doing so (to a lay and impressionable observer), but for real…?

Consider the following: If all cats are crazy, and Jonathan is a cat, then Jonathan is crazy.

This is an example of deduction, one of the three primary modes of reasoning (along with induction and abduction) underlying critical thought and general problem solving. Any advanced AI system currently on the drawing board with ambitions of becoming a general problem solver, or AGI (Artificial General Intelligence), will unavoidably need to perform reliable deduction somehow, either as an explicit high-level function or as an emergent property of its low-level behaviour, and every AI researcher with an interest in AGI – or AI company with ambitions to become an AGI company – needs to know about deduction.

The art of getting a mindless automaton (a.k.a. computer) to perform deduction is called Automated Theorem Proving (ATP), and Professor Paulson has been a recognised world leader in ATP for over 40 years. Who better than Professor Paulson to deliver the inaugural CAIS talk at the Bradfield Centre, Cambridge, on Wednesday 8 March? No one, that’s who!

About the talk

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.


CAIS would not be possible without the support of its sponsors: one-man AGI non-profit BigMother.AI, AI-driven-financial-forecasting startup Dimension Technologies, and (for this event) membership organisation and technology community CW (Cambridge Wireless).

Please note

  • This is an in-person only event, and will not be livestreamed.
  • A recording of the talk, and images of the event, will subsequently be posted online.
  • In particular, CAIS may license the event video to e.g. commercial VoD channels.
  • Please do not attend if you have COVID-, cold-, or flu-like symptoms.
  • Places are strictly limited. Please book early to avoid missing out!
  • CAIS reserve the right to refuse admission to anyone for any reason.

CAIS Talk 08.03.23 - Event Graphic

You can follow @CambWireless on Twitter and tweet about this event using #CWAI.

In collaboration with Cambridge AI Social (CAIS)

Serving the local AI community

View profile


Expand all

The information supplied below may be subject to change before the event.


Pull up a groove and get fabulous! (AKA registration – please arrive early)


Scheduled talk: “Automated Theorem Proving: A Technology Roadmap”


Pizza pizza pizza pizza pizza! (Stimulating conversation encouraged…)


Event close – you don’t have to go home, but you can’t stay here!


Lawrence Paulson - Director of Research, University of Cambridge

Paulson graduated from the California Institute of Technology with a BS in Mathematics in 1977, and obtained a PhD in Computer Science from Stanford University in 1981. After a brief spell as a research assistant at Edinburgh University, Paulson moved to Cambridge University in 1983, where he has been ever since. Elevated to Professor of Computational Logic in 2002, a position he held for 20 years, Paulson has been Director of Research at the University of Cambridge Computer Laboratory since 2022. Paulson was elected Fellow of the ACM (Association of Computing Machinery) in 2008, and Fellow of the Royal Society in 2017. He has been an editor of the Journal of Automated Reasoning for many years, and a trustee of the Conference on Automated Deduction (CADE) since 2010.

SIG Champions

Darendra Appanah - Senior Test Engineer, Cambridge Consultants

Darendra is part of the Systems Engineering & Test department, where he applies his expertise in Digital Security Testing to various technologies, including Machine Learning and AI. He has a background in Software Test Automation of wireless communications protocols, such as satellite communications and LTE. He enjoys defining and developing testing strategies for cybersecurity challenges and ensuring the quality and reliability of innovative solutions.

Maria Axente - Head of AI Public Policy & Ethics, PwC UK

Maria is a globally recognised, award-winning AI ethics public policy expert, a member of various Advisory Boards - UK All-Party Parliamentary Group on AI (APPG AI), NATO EDT & SKEMA AI Institute, and Chair of techUK Data and AI leadership committee. In her current role as Head of AI Public Policy and Ethics, she aligns PwC's AI strategies with ethical considerations and regulatory trends, fostering collaboration with external stakeholders and leading PwC's responses to public policy consultations and initiatives. Maria's commitment to responsible AI has made her a recognised thought leader and influencer in the field. Maria is a passionate advocate for children's rights in the age of AI, serving as a member of the Advisory Board for UNICEF #AI4Children and World Economic Forum Generation AI programmes. She also serves as an Intellectual Forum Senior Research Associate at the University of Cambridge researching human-centric AI and the intersection between tech policy and ethics.

Phil Claridge - Founder, Mandrel Systems

Phil Claridge is a ‘virtual CTO’ for hire within Mandrel Systems covering end-to-end systems. Currently having fun and helping others with large-scale AI systems integration, country-wide large scale big-data processing, hands-on IoT technology (from sensor hardware design, through LoRa integration to back end systems), and advanced city information modelling. Supporting companies with M&A ‘exit readiness’, due-diligence and on advisory boards. Past roles include: CTO, Chief Architect, Labs Director, and Technical Evangelist for Geneva/Convergys (telco), Arieso/Viavi (geolocation), and Madge (networking). Phil’s early career was in electronics, and still finds it irresistible to swap from Powerpoint to a soldering iron and a compiler to produce proof-of-concepts when required.

Parminder Lally - Partner, Appleyard Lees IP LLP

Parminder is a patent attorney based in Appleyard Lees’ Cambridge office, and helps companies to protect their technological innovations. She has built a substantial reputation working with high-growth start-ups, spin-outs and SMEs in Cambridge, and has in-house experience. She specialises in writing and prosecuting patent applications for computer-implemented inventions. Her work includes patenting AI-based technologies, including new machine learning frameworks and applications of machine learning in image classification, human-computer interactions and text-to-speech. Parminder also writes her own AI blog on LinkedIn, and is a member of the Chartered Institute of Patent Attorneys’ Computer Technology Committee.

Simon Thompson - Head of AI, ML & Data Science, GFT Financial Ltd

Simon leads a team that develops AI and ML solutions for large financial institutions. Before joining GFT he was the Principal Investigator for BT’s AI program. Before that he was the Head of Practice for Big Data and Customer Experience at BT and BT’s lead for collaborations with MIT, and the first industry fellow at the Alan Turing Institute. Simon is interested in practical application of AI technology and the practice and process of AI and ML projects. His book “Managing Machine Learning Projects” was published by Manning Books in 2023.

Peter Whale - Programme Manager, UKTIN, Founder & CEO, Vision Formers

Peter is Founder & CEO of Vision Formers, the specialist consultancy that supports and mentors leaders of visionary technology businesses get product to market and turn ideas into reality.

Vision Formers works with start-ups and scale-ups, providing significant expertise in accelerating business growth through a focus on developing a robust product strategy, growing and coaching product and development teams, and providing operational excellence. Peter has a long track record of conceiving, developing and marketing successful technology-based solutions, deployed at scale, globally. Innovative products Peter has brought to market in digital, cloud, AI, consumer electronics and telecommunications have been used by countless millions of people on a daily basis globally, badged by the world’s leading digital and technology brands.

Peter also works with Digital Catapult as Programme Manager for UKTIN, working with partners and stakeholders to deliver UKTIN’s mission to transform the UK telecoms innovation ecosystem, capitalising on the country’s strengths in technology, academia, and entrepreneurialism, while positioning it for growth as new opportunities emerge in the industry.

Peter is a board member of CW (Cambridge Wireless), a Fellow of the IET, a Chartered Engineer, and a member of the Association of Business Mentors.

Event Location

Open in google maps

Location info

The Bradfield Centre, 184 Cambridge Science Park, Milton Road, Cambridge CB4 0GA

Email organiser

Related resources

Related events

  • Cambridge Wireless

    Cambridge Tech Week 2024

    Register now
  • Cambridge Wireless

    RAN architecture evolution towards the 6G vision

    Register now
  • Cambridge Wireless

    CW Collaborate: Enabling Broadband

    Register now

Subscribe to the CW newsletter

This site uses cookies.

We use cookies to help us to improve our site and they enable us to deliver the best possible service and customer experience. By clicking accept or continuing to use this site you are agreeing to our cookies policy. Learn more

Reserve your place

Join the CW network

CW is a leading and vibrant community with a rapidly expanding network of nearly 400 companies across the globe interested in the development and application of wireless and mobile technologies to solve business problems.

Sign in to your account

Please sign in to your CW account to reserve a place at this event and to qualify for any member discounts.

Start typing and press enter or the magnifying glass to search

Sign up to our newsletter
Stay in touch with CW

Choosing to join an existing organisation means that you'll need to be approved before your registration is complete. You'll be notified by email when your request has been accepted.

Your password must be at least 8 characters long and contain at least 1 uppercase character, 1 lowercase character and at least 1 number.

I would like to subscribe to

Select at least one option*