Lawrence Paulson's user avatar
Lawrence Paulson's user avatar
Lawrence Paulson's user avatar
Lawrence Paulson
  • Member for 10 years, 3 months
  • Last seen more than a week ago
Stats
531
reputation
38k
reached
10
answers
2
questions
Loading…
About

I am Professor of Computational Logic at the Computer Laboratory, University of Cambridge, UK. My research concerns automated theorem proving and its applications. I originated and continue to develop the interactive theorem prover Isabelle. I also built MetiTarski, an automatic prover for the elementary functions.

Using Isabelle, I have formalized deep results of set theory: the reflection theorem and the relative consistency of the axiom of choice. I have recently completed the first machine-assisted formalisation of Gödel's second incompleteness theorem. This extends the first incompleteness theorem to state that any suitable formal system that can prove its own consistency is in fact inconsistent.

One of my current research objectives is to unite MetiTarski and Isabelle by formalising in the latter the mathematical facts assumed by the former.

I have a B.S. degree from Caltech in mathematics (covering chiefly logic, but also analysis and combinatorics). My PhD (from Stanford) is in computer science.

This user doesn’t have any gold badges yet.
6
silver badges
11
bronze badges
25
Score
7
Posts
58
Posts %
16
Score
3
Posts
25
Posts %
5
Score
2
Posts
17
Posts %
5
Score
3
Posts
25
Posts %
5
Score
2
Posts
17
Posts %
4
Score
1
Posts
8
Posts %
Top posts
View all questions and answers