Formalizing Ordinal Partition Relations Using Isabelle/HOL
type: Item
instance of: scholarly article
title: Formalizing Ordinal Partition Relations Using Isabelle/HOL
DOI: 10.1080/10586458.2021.1980464
author: Mirna Džamonja
author: Angeliki Koutsoukou-Argyraki
author: Lawrence C. Paulson
published in: Experimental Mathematics
publication date: 2022-08-03T00:00:00Z
full work available at URL: https://arxiv.org/abs/2011.13218
Mathematics Subject Classification ID: 03E02
Mathematics Subject Classification ID: 03E05
Mathematics Subject Classification ID: 03E10
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68V20
Mathematics Subject Classification ID: 68V35
zbMATH DE Number: 7566889
zbMATH Keywords: ordinal partition relations
zbMATH Keywords: set theory
zbMATH Keywords: interactive theorem proving
zbMATH Keywords: Isabelle
zbMATH Keywords: proof assistants
describes a project that uses: Archive Formal Proofs
describes a project that uses: Isabelle/HOL
describes a project that uses: Jordan
describes a project that uses: Automath
describes a project that uses: QuickCheck
describes a project that uses: PVS
describes a project that uses: kepler98
describes a project that uses: HOL Light
describes a project that uses: Nitpick
MaRDI profile type: MaRDI publication profile
OpenAlex ID: W3206346340
cites work: A formally verified proof of the central limit theorem
cites work: Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
cites work: The New Quickcheck for Isabelle
cites work: A partition theorem for the complete graph on \(\omega^\omega\)
cites work: A formulation of the simple theory of types
cites work: Q5573370
cites work: Q3778761
cites work: A partition calculus in set theory
cites work: Combinatorial set theory: Partition relations for cardinals
cites work: A Theorem in the Partition Calculus
cites work: Pinning countable ordinals
cites work: Borel sets and Ramsey's theorem
cites work: Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’
cites work: A FORMAL PROOF OF THE KEPLER CONJECTURE
cites work: The Jordan Curve Theorem, Formally and Informally
cites work: Formalizing an analytic proof of the prime number theorem
cites work: Three Chapters of Measure Theory in Isabelle/HOL
cites work: Q4122841
cites work: Set theory. An introduction to independence proofs
cites work: Analyzing Nash-Williams' partition theorem by means of ordinal types
cites work: A short proof of a partition theorem for the ordinal ωω
cites work: On Fraissé's order type conjecture
cites work: Q3837736
cites work: Q5337204
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: From LCF to Isabelle/HOL
cites work: Countable partition ordinals
cites work: Teilmengen von Mengen mit Relationen
cites work: Partitioning pairs of countable ordinals
cites work: Partition Problems in Topology
cites work: Introduction to Ramsey Spaces (AM-174)
cites work: A synthesis of the procedural and declarative styles of interactive theorem proving
description: scientific article; zbMATH DE number 7566889