Lawrence C. Paulson

ORCID

Publication Activity (10 Years)

Years Active: 1982-2024
Publications (10 Years): 80

Top Venues

Publications

Chelsea Edmonds, Lawrence C. Paulson
Formal Probabilistic Methods for Combinatorial Structures using the Lovász Local Lemma. CPP (2024)
Lawrence C. Paulson
A formalised theorem in the partition calculus. Ann. Pure Appl. Log. 175 (Issue 1, Part B) (2024)
Chelsea Edmonds, Lawrence C. Paulson
Formal Probabilistic Methods for Combinatorial Structures in Isabelle/HOL. CoRR (2023)
Lawrence C. Paulson
Knuth-Morris-Pratt String Search. Arch. Formal Proofs 2023 (2023)
Chelsea Edmonds, Lawrence C. Paulson
Hypergraph Colouring Bounds. Arch. Formal Proofs 2023 (2023)
Chelsea Edmonds, Lawrence C. Paulson
Hypergraph Colouring Bounds. Arch. Formal Proofs 2023 (2023)
Lawrence C. Paulson
Euler's Polyhedron Formula. Arch. Formal Proofs 2023 (2023)
Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson
Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL. J. Autom. Reason. 67 (1) (2023)
Lawrence C. Paulson
Large-Scale Formal Proof for the Working Mathematician - Lessons Learnt from the ALEXANDRIA Project. CICM (2023)
Lawrence C. Paulson
Irrational numbers from THE BOOK. Arch. Formal Proofs 2022 (2022)
Lawrence C. Paulson
Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis. CICM (2022)
Chaitanya Mangla, Sean B. Holden, Lawrence C. Paulson
Bayesian Ranking for Strategy Scheduling in Automated Theorem Provers. IJCAR (2022)
Jonas Bayer, Christoph Benzmüller, Kevin Buzzard, Marco David, Leslie Lamport, Yuri V. Matiyasevich, Lawrence C. Paulson, Dierk Schleicher, Benedikt Stock, Efim I. Zelmanov
Mathematical Proof Between Generations. CoRR (2022)
Chelsea Edmonds, Lawrence C. Paulson
Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics. CoRR (2022)
Jacques D. Fleuriot, Lawrence C. Paulson
Constructing the Reals as Dedekind Cuts of Rationals. Arch. Formal Proofs 2022 (2022)
Mirna Dzamonja, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson
Formalizing Ordinal Partition Relations Using Isabelle/HOL. Exp. Math. 31 (2) (2022)
Anthony Bordg, Lawrence C. Paulson, Wenda Li
Simple Type Theory is not too Simple: Grothendieck's Schemes Without Dependent Types. Exp. Math. 31 (2) (2022)
Lawrence C. Paulson
Wetzel: Formalisation of an Undecidable Problem Linked to the Continuum Hypothesis. CoRR (2022)
Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson
The Plünnecke-Ruzsa Inequality. Arch. Formal Proofs 2022 (2022)
Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson
Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL. CoRR (2022)
Samuel Coward, Lawrence C. Paulson, Theo Drane, Emiliano Morini
Formal Verification of Transcendental Fixed- and Floating-point Algorithms using an Automatic Theorem Prover. Formal Aspects Comput. 34 (2) (2022)
Chelsea Edmonds, Lawrence C. Paulson
Fisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics. Arch. Formal Proofs 2022 (2022)
Lawrence C. Paulson
Wetzel's Problem and the Continuum Hypothesis. Arch. Formal Proofs 2022 (2022)
Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson
Khovanskii's Theorem. Arch. Formal Proofs 2022 (2022)
Lawrence C. Paulson
Young's Inequality for Increasing Functions. Arch. Formal Proofs 2022 (2022)
Chelsea Edmonds, Lawrence C. Paulson
Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics. ITP (2022)
Lawrence C. Paulson
Ackermann's Function Is Not Primitive Recursive. Arch. Formal Proofs 2022 (2022)
Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence C. Paulson
Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL. Exp. Math. 31 (2) (2022)
Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson
Szemerédi's Regularity Lemma. Arch. Formal Proofs 2021 (2021)
Lawrence C. Paulson
A Mechanised Proof of Gödel's Incompleteness Theorems using Nominal Isabelle. CoRR (2021)
Chelsea Edmonds, Lawrence C. Paulson
Combinatorial Design Theory. Arch. Formal Proofs 2021 (2021)
Chelsea Edmonds, Lawrence C. Paulson
A Modular First Formalisation of Combinatorial Design Theory. CICM (2021)
Chelsea Edmonds, Lawrence C. Paulson
A Modular First Formalisation of Combinatorial Design Theory. CoRR (2021)
Chelsea Edmonds, Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson
Roth's Theorem on Arithmetic Progressions. Arch. Formal Proofs 2021 (2021)
Lawrence C. Paulson
The Inductive Approach to Verifying Cryptographic Protocols. CoRR (2021)
Lawrence C. Paulson
Ackermann's function in iterative Form: a Proof Assistant Experiment. Bull. Symb. Log. 27 (4) (2021)
Wenda Li, Lei Yu, Yuhuai Wu, Lawrence C. Paulson
IsarStep: a Benchmark for High-level Mathematical Reasoning. ICLR (2021)
Angeliki Koutsoukou-Argyraki, Wenda Li, Lawrence C. Paulson
Irrationality and Transcendence Criteria for Infinite Series in Isabelle/HOL. CoRR (2021)
Lawrence C. Paulson
The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle/ZF. CoRR (2021)
Anthony Bordg, Lawrence C. Paulson, Wenda Li
Grothendieck's Schemes in Algebraic Geometry. Arch. Formal Proofs 2021 (2021)
Anthony Bordg, Lawrence C. Paulson, Wenda Li
Simple Type Theory is not too Simple: Grothendieck's Schemes without Dependent Types. CoRR (2021)
Lawrence C. Paulson
Ackermann's Function in Iterative Form: A Proof Assistant Experiment. CoRR (2021)
Agnieszka Slowik, Chaitanya Mangla, Mateja Jamnik, Sean B. Holden, Lawrence C. Paulson
Bayesian Optimisation for Premise Selection in Automated Theorem Proving (Student Abstract). AAAI (2020)
Wenda Li, Lei Yu, Yuhuai Wu, Lawrence C. Paulson
Modelling High-Level Mathematical Reasoning in Mechanised Declarative Proofs. CoRR (2020)
Lawrence C. Paulson
The Nash-Williams Partition Theorem. Arch. Formal Proofs 2020 (2020)
Wenda Li, Lawrence C. Paulson
Evaluating Winding Numbers and Counting Complex Roots Through Cauchy Indices in Isabelle/HOL. J. Autom. Reason. 64 (2) (2020)
Paulo Emílio de Vilhena, Lawrence C. Paulson
Algebraically Closed Fields in Isabelle/HOL. IJCAR (2) (2020)
Lawrence C. Paulson
Ordinal Partitions. Arch. Formal Proofs 2020 (2020)
Chaitanya Mangla, Sean B. Holden, Lawrence C. Paulson
Bayesian Optimisation of Solver Parameters in CBMC. SMT (2020)
Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel
From LCF to Isabelle/HOL. CoRR (2019)
Wenda Li, Lawrence C. Paulson
Counting polynomial roots in isabelle/hol: a formal proof of the budan-fourier theorem. CPP (2019)
Mohammad Abdulaziz, Lawrence C. Paulson
An Isabelle/HOL Formalisation of Green's Theorem. J. Autom. Reason. 63 (3) (2019)
Lawrence C. Paulson
Inductive Analysis of the Internet Protocol TLS. CoRR (2019)
Lawrence C. Paulson, Tobias Nipkow, Makarius Wenzel
From LCF to Isabelle/HOL. Formal Aspects Comput. 31 (6) (2019)
Agnieszka Slowik, Chaitanya Mangla, Mateja Jamnik, Sean B. Holden, Lawrence C. Paulson
Bayesian Optimisation with Gaussian Processes for Premise Selection. CoRR (2019)
Lawrence C. Paulson
Defining Functions on Equivalence Classes. CoRR (2019)
Agnieszka Slowik, Chaitanya Mangla, Mateja Jamnik, Sean B. Holden, Lawrence C. Paulson
Bayesian Optimisation for Heuristic Configuration in Automated Theorem Proving. Vampire (2019)
Lawrence C. Paulson
Fourier Series. Arch. Formal Proofs 2019 (2019)
Wenda Li, Grant Olney Passmore, Lawrence C. Paulson
Deciding Univariate Polynomial Problems Using Untrusted Certificates in Isabelle/HOL. J. Autom. Reason. 62 (1) (2019)
Lawrence C. Paulson
Zermelo Fraenkel Set Theory in Higher-Order Logic. Arch. Formal Proofs 2019 (2019)
Zongyan Huang, Matthew England, David J. Wilson, James P. Bridge, James H. Davenport, Lawrence C. Paulson
Using Machine Learning to Improve Cylindrical Algebraic Decomposition. Math. Comput. Sci. 13 (4) (2019)
Wenda Li, Lawrence C. Paulson
Evaluating Winding Numbers and Counting Complex Roots through Cauchy Indices in Isabelle/HOL. CoRR (2018)
Lawrence C. Paulson
Quaternions. Arch. Formal Proofs 2018 (2018)
Lawrence C. Paulson
Michael John Caldwell Gordon (FRS 1994), 28 February 1948 - 22 August 2017. CoRR (2018)
Lawrence C. Paulson
Formalising Mathematics In Simple Type Theory. CoRR (2018)
Zongyan Huang, Matthew England, David J. Wilson, James H. Davenport, Lawrence C. Paulson
Using Machine Learning to Improve Cylindrical Algebraic Decomposition. CoRR (2018)
Mohammad Abdulaziz, Lawrence C. Paulson
An Isabelle/HOL formalisation of Green's Theorem. Arch. Formal Proofs 2018 (2018)
Jeremy Avigad, Jasmin Christian Blanchette, Gerwin Klein, Lawrence C. Paulson, Andrei Popescu, Gregor Snelting
Introduction to Milestones in Interactive Theorem Proving. J. Autom. Reason. 61 (1-4) (2018)
Wenda Li, Lawrence C. Paulson
Counting Polynomial Roots in Isabelle/HOL: A Formal Proof of the Budan-Fourier Theorem. CoRR (2018)
Manuel Eberl, Lawrence C. Paulson
The Prime Number Theorem. Arch. Formal Proofs 2018 (2018)
Lawrence C. Paulson
Computational Logic: Its Origins and Applications. CoRR (2017)
Lawrence C. Paulson
Porting the HOL light analysis library: some lessons (invited talk). CPP (2017)
Wenda Li, Lawrence C. Paulson
A modular, efficient formalisation of real algebraic numbers. CPP (2016)
Wenda Li, Lawrence C. Paulson
A Formal Proof of Cauchy's Residue Theorem. ITP (2016)
Lawrence C. Paulson
The Cartan Fixed Point Theorems. Arch. Formal Proofs 2016 (2016)
Quentin Hibon, Lawrence C. Paulson
Source Coding Theorem. Arch. Formal Proofs 2016 (2016)
Zongyan Huang, Matthew England, James H. Davenport, Lawrence C. Paulson
Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition with Groebner Bases. SYNASC (2016)
Mohammad Abdulaziz, Lawrence C. Paulson
An Isabelle/HOL Formalisation of Green's Theorem. ITP (2016)
Zongyan Huang, Matthew England, James H. Davenport, Lawrence C. Paulson
Using Machine Learning to Decide When to Precondition Cylindrical Algebraic Decomposition With Groebner Bases. CoRR (2016)
Jasmin Christian Blanchette, Cezary Kaliszyk, Lawrence C. Paulson, Josef Urban
Hammering towards QED. J. Formaliz. Reason. 9 (1) (2016)
Wenda Li, Grant Olney Passmore, Lawrence C. Paulson
A Complete Decision Procedure for Univariate Polynomial Problems in Isabelle/HOL. CoRR (2015)
Lawrence C. Paulson
Finite Automata in Hereditarily Finite Set Theory. Arch. Formal Proofs 2015 (2015)
Nik Sultana, Christoph Benzmüller, Lawrence C. Paulson
Proofs and Reconstructions. FroCos (2015)
Lawrence C. Paulson
A Formalisation of Finite Automata Using Hereditarily Finite Sets. CADE (2015)
Lawrence C. Paulson
A Mechanised Proof of Gödel's Incompleteness Theorems Using Nominal Isabelle. J. Autom. Reason. 55 (1) (2015)
Lawrence C. Paulson
A Formalisation of Finite Automata using Hereditarily Finite Sets. CoRR (2015)
Christoph Benzmüller, Nik Sultana, Lawrence C. Paulson, Frank Theiss
The Higher-Order Prover Leo-II. J. Autom. Reason. 55 (4) (2015)
Jean Everson Martina, Lawrence C. Paulson
Verifying multicast-based security protocols using the inductive method. Int. J. Inf. Sec. 14 (2) (2015)
Paul B. Jackson, Andrew Sogokon, James P. Bridge, Lawrence C. Paulson
Verifying Hybrid Systems Involving Transcendental Functions. NASA Formal Methods (2014)
Zongyan Huang, Matthew England, David J. Wilson, James H. Davenport, Lawrence C. Paulson
A comparison of three heuristics to choose the variable ordering for CAD. CoRR (2014)
Lawrence C. Paulson
Real-Valued Special Functions: Upper and Lower Bounds. Arch. Formal Proofs 2014 (2014)
Lawrence C. Paulson
A Machine-Assisted Proof of Gödel's Incompleteness theorems for the Theory of Hereditarily Finite Sets. Rev. Symb. Log. 7 (3) (2014)
Zongyan Huang, Matthew England, David J. Wilson, James H. Davenport, Lawrence C. Paulson, James P. Bridge
Applying Machine Learning to the Problem of Choosing a Heuristic to Select the Variable Ordering for Cylindrical Algebraic Decomposition. CICM (2014)
Zongyan Huang, Matthew England, David J. Wilson, James H. Davenport, Lawrence C. Paulson
A Comparison of Three Heuristics to Choose the Variable Ordering for Cylindrical Algebraic Decomposition. ACM Commun. Comput. Algebra 48 (3/4) (2014)
Zongyan Huang, Matthew England, David J. Wilson, James H. Davenport, Lawrence C. Paulson, James P. Bridge
Applying machine learning to the problem of choosing a heuristic to select the variable ordering for cylindrical algebraic decomposition. CoRR (2014)
James P. Bridge, Sean B. Holden, Lawrence C. Paulson
Machine Learning for First-Order Theorem Proving - Learning to Select a Good Heuristic. J. Autom. Reason. 53 (2) (2014)
Lawrence C. Paulson
Automated theorem proving for special functions: the next phase. SNC (2014)
Lawrence C. Paulson
The Hereditarily Finite Sets. Arch. Formal Proofs 2013 (2013)
Jean Everson Martina, Lawrence C. Paulson
Verifying multicast-based security protocols using the inductive method. SAC (2013)
Lawrence C. Paulson
MetiTarski's Menagerie of Cooperating Systems. FroCos (2013)

Lawrence C. Paulson.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Lawrence C. Paulson