{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:58:57Z","timestamp":1759147137523,"version":"3.37.3"},"reference-count":46,"publisher":"Informa UK Limited","issue":"2","license":[{"start":{"date-parts":[[2021,10,11]],"date-time":"2021-10-11T00:00:00Z","timestamp":1633910400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000608","name":"London Mathematical Society","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100000608","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["www.tandfonline.com"],"crossmark-restriction":true},"short-container-title":["Experimental Mathematics"],"published-print":{"date-parts":[[2022,4,3]]},"DOI":"10.1080\/10586458.2021.1980464","type":"journal-article","created":{"date-parts":[[2021,10,14]],"date-time":"2021-10-14T02:44:56Z","timestamp":1634179496000},"page":"383-400","update-policy":"https:\/\/doi.org\/10.1080\/tandf_crossmark_01","source":"Crossref","is-referenced-by-count":5,"title":["Formalizing Ordinal Partition Relations Using Isabelle\/HOL"],"prefix":"10.1080","volume":"31","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6771-3975","authenticated-orcid":false,"given":"Mirna","family":"D\u017eamonja","sequence":"first","affiliation":[{"name":"IRIF, CNRS-Universit\u00e9 de Paris, Paris, France"},{"name":"Institute of Mathematics, Czech Academy of Sciences, Prague, Czech Republic;"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8886-5281","authenticated-orcid":false,"given":"Angeliki","family":"Koutsoukou-Argyraki","sequence":"additional","affiliation":[{"name":"Computer Laboratory, University of Cambridge, Cambridge, UK"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0288-4279","authenticated-orcid":false,"given":"Lawrence C.","family":"Paulson","sequence":"additional","affiliation":[{"name":"Computer Laboratory, University of Cambridge, Cambridge, UK"}]}],"member":"301","published-online":{"date-parts":[[2021,10,11]]},"reference":[{"key":"CIT0001","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9404-x"},{"key":"CIT0002","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14052-5_11"},{"key":"CIT0003","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35308-6_10"},{"key":"CIT0004","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-30229-0_1"},{"key":"CIT0005","doi-asserted-by":"publisher","DOI":"10.1016\/0097-3165(72)90105-7"},{"key":"CIT0006","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"volume-title":"Set Theory and the Continuum Hypothesis","year":"1966","author":"Cohen P.","key":"CIT0007"},{"key":"CIT0008","doi-asserted-by":"publisher","DOI":"10.1017\/9781108303866"},{"key":"CIT0009","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/065\/891250"},{"key":"CIT0010","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9904-1956-10036-0"},{"volume-title":"Combinatorial Set Theory: Partition Relations for Cardinals","year":"1984","author":"Erd\u00f6s P.","key":"CIT0011"},{"key":"CIT0012","doi-asserted-by":"publisher","DOI":"10.4153\/CMB-1972-088-1"},{"key":"CIT0013","doi-asserted-by":"publisher","DOI":"10.4153\/CMB-1974-062-6"},{"key":"CIT0014","doi-asserted-by":"publisher","DOI":"10.4064\/fm-82-4-357-361"},{"key":"CIT0015","doi-asserted-by":"publisher","DOI":"10.2307\/2272055"},{"key":"CIT0016","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.2014.0234"},{"key":"CIT0017","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-5764-9_3"},{"key":"CIT0018","doi-asserted-by":"publisher","DOI":"10.1017\/fmp.2017.1"},{"key":"CIT0019","doi-asserted-by":"publisher","DOI":"10.1080\/00029890.2007.11920481"},{"key":"CIT0020","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008712907154"},{"key":"CIT0021","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9145-6"},{"key":"CIT0022","unstructured":"Hodkinson, I. (2003). Kruskal\u2019s theorem and Nash-Williams theory, after Wilfrid Hodges. version 3.6. Available at: www.doc.ic.ac.uk\/imh\/papers\/bar.pdf, February."},{"key":"CIT0023","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22863-6_12"},{"key":"CIT0024","unstructured":"van Benthem Jutting, L.S. (1977).Checking Landau\u2019s \u201cGrundlagen\u201d in the AUTOMATH System. PhD thesis, Eindhoven University of Technology. doi:10.6100\/IR23183."},{"key":"CIT0025","doi-asserted-by":"publisher","DOI":"10.1109\/HOL.1991.596266"},{"volume-title":"Set Theory, volume 102 of Studies in Logic and the Foundations of Mathematics","year":"1980","author":"Kunen K.","key":"CIT0026"},{"key":"CIT0027","doi-asserted-by":"publisher","DOI":"10.1016\/0012-365X(91)90334-X"},{"key":"CIT0028","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4843(73)90006-5"},{"key":"CIT0029","doi-asserted-by":"publisher","DOI":"10.2307\/1970754"},{"key":"CIT0030","doi-asserted-by":"crossref","first-page":"327","DOI":"10.1093\/oso\/9780198538622.003.0014","volume-title":"Logic: from Foundations to Applications; European logic colloquium","author":"Marcone A.","year":"1996"},{"key":"CIT0031","doi-asserted-by":"publisher","DOI":"10.1017\/S0305004100038603"},{"key":"CIT0032","unstructured":"Nicely, T. R. Pentium FDIV flaw, 2011. FAQ. Available at: https:\/\/faculty.lynchburg.edu\/nicely\/pentbug\/pentbug.html."},{"key":"CIT0033","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9"},{"key":"CIT0034","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61474-5_91"},{"key":"CIT0035","unstructured":"Paulson, L. C. (2019). Zermelo Fraenkel set theory in higher-order logic.Archive of Formal Proofs, October. Available at: http:\/\/isa-afp.org\/entries\/ZFC_in_HOL.html, Formal proof development."},{"key":"CIT0036","unstructured":"Paulson, L. C. (2020). The Nash-Williams partition theorem.Archive of Formal Proofs, May. Available at: http:\/\/isa-afp.org\/entries\/Nash_Williams.html, Formal proof development."},{"key":"CIT0037","unstructured":"Paulson, L. C. (2020).Ordinal partitions.Archive of Formal Proofs, August. Available at: http:\/\/isa-afp.org\/entries\/Ordinal_Partitions.html, Formal proof development."},{"key":"CIT0038","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00492-1"},{"issue":"4","key":"CIT0039","first-page":"264","volume":"30","author":"Ramsey F. P.","year":"1929","journal-title":"Proc. London Math. Soc. (2)"},{"key":"CIT0040","unstructured":"Schipperus, R. (1999). Countable partition ordinals. PhD thesis, University of Colorado-Boulder."},{"key":"CIT0041","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2009.12.007"},{"key":"CIT0042","doi-asserted-by":"publisher","DOI":"10.1007\/BF02564361"},{"key":"CIT0043","doi-asserted-by":"publisher","DOI":"10.1007\/BF02392561"},{"key":"CIT0044","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/084"},{"key":"CIT0045","doi-asserted-by":"publisher","DOI":"10.1515\/9781400835409"},{"volume-title":"Technical report","year":"2000","author":"Wiedijk. Freek","key":"CIT0046"}],"container-title":["Experimental Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.tandfonline.com\/doi\/pdf\/10.1080\/10586458.2021.1980464","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,11,11]],"date-time":"2023-11-11T03:36:10Z","timestamp":1699673770000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.tandfonline.com\/doi\/full\/10.1080\/10586458.2021.1980464"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,11]]},"references-count":46,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,4,3]]}},"alternative-id":["10.1080\/10586458.2021.1980464"],"URL":"https:\/\/doi.org\/10.1080\/10586458.2021.1980464","relation":{},"ISSN":["1058-6458","1944-950X"],"issn-type":[{"type":"print","value":"1058-6458"},{"type":"electronic","value":"1944-950X"}],"subject":[],"published":{"date-parts":[[2021,10,11]]},"assertion":[{"value":"The publishing and review policy for this title is described in its Aims & Scope.","order":1,"name":"peerreview_statement","label":"Peer Review Statement"},{"value":"http:\/\/www.tandfonline.com\/action\/journalInformation?show=aimsScope&journalCode=uexm20","URL":"http:\/\/www.tandfonline.com\/action\/journalInformation?show=aimsScope&journalCode=uexm20","order":2,"name":"aims_and_scope_url","label":"Aim & Scope"},{"value":"2021-10-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}