Formalizing Ordinal Partition Relations Using Isabelle/HOL
Repository URI
Repository DOI
Change log
Authors
Džamonja, M https://orcid.org/0000-0002-6771-3975
Koutsoukou-Argyraki, A https://orcid.org/0000-0002-8886-5281
Paulson, LC https://orcid.org/0000-0003-0288-4279
Abstract
This is an overview of a formalisation project in the proof assistant
Isabelle/HOL of a number of research results in infinitary combinatorics and
set theory (more specifically in ordinal partition relations) by
Erd\H{o}s--Milner, Specker, Larson and Nash-Williams, leading to Larson's proof
of the unpublished result by E.C. Milner asserting that for all
Description
Keywords
Ordinal partition relations, set theory, interactive theorem proving, Isabelle, proof assistants
Journal Title
Experimental Mathematics
Conference Name
Journal ISSN
1058-6458
1944-950X
1944-950X
Volume Title
Publisher
Informa UK Limited
Publisher DOI
Sponsorship
European Research Council (742178)