Vše

Co hledáte?

Vše
Projekty
Výsledky výzkumu
Subjekty

Rychlé hledání

  • Projekty podpořené TA ČR
  • Významné projekty
  • Projekty s nejvyšší státní podporou
  • Aktuálně běžící projekty

Chytré vyhledávání

  • Takto najdu konkrétní +slovo
  • Takto z výsledků -slovo zcela vynechám
  • “Takto můžu najít celou frázi”

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