Formalizing ordinal partition relations using Isabelle/HOL
Identifikátory výsledku
Kód výsledku v 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>
Výsledek na webu
<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>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Formalizing ordinal partition relations using Isabelle/HOL
Popis výsledku v původním jazyce
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.
Název v anglickém jazyce
Formalizing ordinal partition relations using Isabelle/HOL
Popis výsledku anglicky
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.
Klasifikace
Druh
J<sub>imp</sub> - Článek v periodiku v databázi Web of Science
CEP obor
—
OECD FORD obor
10101 - Pure mathematics
Návaznosti výsledku
Projekt
<a href="/cs/project/GX20-31529X" target="_blank" >GX20-31529X: Abstraktní konvergenční schémata a jejich složitost</a><br>
Návaznosti
I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Ostatní
Rok uplatnění
2022
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název periodika
Experimental Mathematics
ISSN
1058-6458
e-ISSN
1944-950X
Svazek periodika
31
Číslo periodika v rámci svazku
2
Stát vydavatele periodika
US - Spojené státy americké
Počet stran výsledku
18
Strana od-do
383-400
Kód UT WoS článku
000706273600001
EID výsledku v databázi Scopus
2-s2.0-85116784275