0559684 - MÚ 2023 RIV US eng J - Článek v odborném periodiku
Džamonja, Mirna - Koutsoukou-Argyraki, A. - Paulson, L. C.
Formalizing ordinal partition relations using Isabelle/HOL.
Experimental Mathematics. Roč. 31, č. 2 (2022), s. 383-400. ISSN 1058-6458. E-ISSN 1944-950X
Grant CEP: GA ČR(CZ) GX20-31529X
Institucionální podpora: RVO:67985840
Klíčová slova: interactive theorem proving * Isabelle * ordinal partition relations * set theory
Obor OECD: Pure mathematics
Impakt faktor: 0.5, rok: 2022
Způsob publikování: Open access
https://doi.org/10.1080/10586458.2021.1980464

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.
Trvalý link: https://hdl.handle.net/11104/0332887