Zobrazeno 1 - 10
of 252
pro vyhledávání: '"Paulson, Lawrence C."'
Autor:
Edmonds, Chelsea, Paulson, Lawrence C.
Formalised libraries of combinatorial mathematics have rapidly expanded over the last five years, but few use one of the most important tools: probability. How can often intuitive probabilistic arguments on the existence of combinatorial structures,
Externí odkaz:
http://arxiv.org/abs/2310.00513
Large-Scale Formal Proof for the Working Mathematician -- Lessons learnt from the ALEXANDRIA Project
Autor:
Paulson, Lawrence C
ALEXANDRIA is an ERC-funded project that started in 2017, with the aim of bringing formal verification to mathematics. The past six years have seen great strides in the formalisation of mathematics and also in some relevant technologies, above all ma
Externí odkaz:
http://arxiv.org/abs/2305.14407
We have formalised Szemer\'edi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions, two major results in extremal graph theory and additive combinatorics, using the proof assistant Isabelle/HOL. For the latter formalisation, we used the
Externí odkaz:
http://arxiv.org/abs/2207.07499
Autor:
Edmonds, Chelsea, Paulson, Lawrence C.
Publikováno v:
13th International Conference on Interactive Theorem Proving (2022). 11:1-11:19
The formalisation of mathematics is continuing rapidly, however combinatorics continues to present challenges to formalisation efforts, such as its reliance on techniques from a wide range of other fields in mathematics. This paper presents formal li
Externí odkaz:
http://arxiv.org/abs/2207.02728
Autor:
Paulson, Lawrence C
Publikováno v:
In: Buzzard, K., Kutsia, T. (eds) Intelligent Computer Mathematics. CICM 2022
In 1964, Paul Erd\H{o}s published a paper settling a question about function spaces that he had seen in a problem book. Erd\H{o}s proved that the answer was yes if and only if the continuum hypothesis was false: an innocent-looking question turned ou
Externí odkaz:
http://arxiv.org/abs/2205.03159
Autor:
Paulson, Lawrence C.
Publikováno v:
J. Computer Security 6 (1998), 85-128
Informal arguments that cryptographic protocols are secure can be made rigorous using inductive definitions. The approach is based on ordinary predicate calculus and copes with infinite-state systems. Proofs are generated using Isabelle/HOL. The huma
Externí odkaz:
http://arxiv.org/abs/2105.06319
Autor:
Paulson, Lawrence C.
Publikováno v:
Review of Symbolic Logic 7:3 (2014), 484-498
A formalisation of G\"odel's incompleteness theorems using the Isabelle proof assistant is described. This is apparently the first mechanical verification of the second incompleteness theorem. The work closely follows {\'S}wierczkowski (2003), who ga
Externí odkaz:
http://arxiv.org/abs/2104.14260
Autor:
Paulson, Lawrence C.
Publikováno v:
J Autom Reasoning 55, 1-37 (2015)
An Isabelle/HOL formalisation of G\"odel's two incompleteness theorems is presented. The work follows \'Swierczkowski's detailed proof of the theorems using hereditarily finite (HF) set theory. Avoiding the usual arithmetical encodings of syntax elim
Externí odkaz:
http://arxiv.org/abs/2104.13792
Autor:
Paulson, Lawrence C.
Publikováno v:
LMS Journal of Computation and Mathematics, Volume 6, 2003, pp. 198-248
The proof of the relative consistency of the axiom of choice has been mechanized using Isabelle/ZF. The proof builds upon a previous mechanization of the reflection theorem. The heavy reliance on metatheory in the original proof makes the formalizati
Externí odkaz:
http://arxiv.org/abs/2104.12674
Autor:
Paulson, Lawrence C.
A paper on ordinal partitions by Erd\H{o}s and Milner (1972) has been formalised using the proof assistant Isabelle/HOL, augmented with a library for Zermelo-Fraenkel set theory. The work is part of a project on formalising the partition calculus. Th
Externí odkaz:
http://arxiv.org/abs/2104.11613