Počet záznamů: 1
Formalizing ordinal partition relations using Isabelle/HOL
- 1.
SYSNO ASEP 0559684 Druh ASEP J - Článek v odborném periodiku Zařazení RIV J - Článek v odborném periodiku Poddruh J Článek ve WOS Název Formalizing ordinal partition relations using Isabelle/HOL Tvůrce(i) Džamonja, Mirna (MU-W) SAI, ORCID, RID
Koutsoukou-Argyraki, A. (GB)
Paulson, L. C. (GB)Zdroj.dok. Experimental Mathematics. - : Taylor & Francis - ISSN 1058-6458
Roč. 31, č. 2 (2022), s. 383-400Poč.str. 18 s. Jazyk dok. eng - angličtina Země vyd. US - Spojené státy americké Klíč. slova interactive theorem proving ; Isabelle ; ordinal partition relations ; set theory Vědní obor RIV BA - Obecná matematika Obor OECD Pure mathematics CEP GX20-31529X GA ČR - Grantová agentura ČR Způsob publikování Open access Institucionální podpora MU-W - RVO:67985840 UT WOS 000706273600001 EID SCOPUS 85116784275 DOI https://doi.org/10.1080/10586458.2021.1980464 Anotace 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. Pracoviště Matematický ústav Kontakt Jarmila Štruncová, struncova@math.cas.cz, library@math.cas.cz, Tel.: 222 090 757 Rok sběru 2023 Elektronická adresa https://doi.org/10.1080/10586458.2021.1980464
Počet záznamů: 1