Formalizing ordinal partition relations using Isabelle/HOL
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985840%3A_____%2F22%3A00559684" target="_blank" >RIV/67985840:_____/22:00559684 - isvavai.cz</a>
Result on the web
<a href="https://doi.org/10.1080/10586458.2021.1980464" target="_blank" >https://doi.org/10.1080/10586458.2021.1980464</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1080/10586458.2021.1980464" target="_blank" >10.1080/10586458.2021.1980464</a>
Alternative languages
Result language
angličtina
Original language name
Formalizing ordinal partition relations using Isabelle/HOL
Original language description
This is an overview of a formalization 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ős-Milner, Specker, Larson and Nash-Williams, leading to Larson’s proof of the unpublished result by E.C. Milner asserting that for all (Formula presented.), (Formula presented.). This material has been recently formalised by Paulson and is available on the Archive of Formal Proofs, here we discuss some of the most challenging aspects of the formalization process. This project is also a demonstration of working with Zermelo–Fraenkel set theory in higher-order logic.
Czech name
—
Czech description
—
Classification
Type
J<sub>imp</sub> - Article in a specialist periodical, which is included in the Web of Science database
CEP classification
—
OECD FORD branch
10101 - Pure mathematics
Result continuities
Project
<a href="/en/project/GX20-31529X" target="_blank" >GX20-31529X: Abstract convergence schemes and their complexities</a><br>
Continuities
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Others
Publication year
2022
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
Experimental Mathematics
ISSN
1058-6458
e-ISSN
1944-950X
Volume of the periodical
31
Issue of the periodical within the volume
2
Country of publishing house
US - UNITED STATES
Number of pages
18
Pages from-to
383-400
UT code for WoS article
000706273600001
EID of the result in the Scopus database
2-s2.0-85116784275