Formalizing Ordinal Partition Relations Using Isabelle/HOL
From MaRDI portal
Publication:5094473
DOI10.1080/10586458.2021.1980464OpenAlexW3206346340MaRDI QIDQ5094473
Angeliki Koutsoukou-Argyraki, Mirna Dzamonja, Lawrence Charles Paulson
Publication date: 3 August 2022
Published in: Experimental Mathematics (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2011.13218
Mechanization of proofs and logical operations (03B35) Other combinatorial set theory (03E05) Partition relations (03E02) Ordinal and cardinal numbers (03E10) Formalization of mathematics in connection with theorem provers (68V20) Digital mathematics libraries and repositories (68V35)
Related Items (6)
A formalised theorem in the partition calculus ⋮ Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project ⋮ The formal verification of the ctm approach to forcing ⋮ Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL ⋮ Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis ⋮ Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Countable partition ordinals
- Teilmengen von Mengen mit Relationen
- Combinatorial set theory: Partition relations for cardinals
- Partitioning pairs of countable ordinals
- Set theory. An introduction to independence proofs
- Analyzing Nash-Williams' partition theorem by means of ordinal types
- Isabelle/HOL. A proof assistant for higher-order logic
- A formally verified proof of the central limit theorem
- From LCF to Isabelle/HOL
- On Fraissé's order type conjecture
- A partition theorem for the complete graph on \(\omega^\omega\)
- Formalizing an analytic proof of the prime number theorem
- A Synthesis of the Procedural and Declarative Styles of Interactive Theorem Proving
- Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’
- Three Chapters of Measure Theory in Isabelle/HOL
- A Theorem in the Partition Calculus
- A partition calculus in set theory
- Introduction to Ramsey Spaces (AM-174)
- Partition Problems in Topology
- Pinning countable ordinals
- Borel sets and Ramsey's theorem
- The New Quickcheck for Isabelle
- A short proof of a partition theorem for the ordinal ωω
- A FORMAL PROOF OF THE KEPLER CONJECTURE
- The Jordan Curve Theorem, Formally and Informally
- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
- A formulation of the simple theory of types
This page was built for publication: Formalizing Ordinal Partition Relations Using Isabelle/HOL
