Skip to main content
Lawrence Paulson's user avatar
Lawrence Paulson's user avatar
Lawrence Paulson's user avatar
Lawrence Paulson
  • Member for 2 years, 3 months
  • Last seen more than a month ago
Stats
806
reputation
7k
reached
8
answers
0
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.
3
silver badges
6
bronze badges
18
Score
2
Posts
25
Posts %
13
Score
2
Posts
25
Posts %
13
Score
1
Posts
12
Posts %
13
Score
1
Posts
12
Posts %
12
Score
1
Posts
12
Posts %
12
Score
1
Posts
12
Posts %
Top posts