Formalizing ordinal partition relations using Isabelle/HOL
DOI10.1080/10586458.2021.1980464OpenAlexW3206346340MaRDI QIDQ5094473FDOQ5094473
Authors: Mirna Džamonja, Angeliki Koutsoukou-Argyraki, Lawrence C. 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
Recommendations
Mechanization of proofs and logical operations (03B35) Partition relations (03E02) Other combinatorial set theory (03E05) Formalization of mathematics in connection with theorem provers (68V20) Ordinal and cardinal numbers (03E10) Digital mathematics libraries and repositories (68V35)
Cites Work
- Title not available (Why is that?)
- Nitpick: a counterexample generator for higher-order logic based on a relational model finder
- A synthesis of the procedural and declarative styles of interactive theorem proving
- Set theory. An introduction to independence proofs
- Isabelle/HOL. A proof assistant for higher-order logic
- On Fraissé's order type conjecture
- Borel sets and Ramsey's theorem
- Title not available (Why is that?)
- A formulation of the simple theory of types
- Partitioning pairs of countable ordinals
- A formally verified proof of the central limit theorem
- Partition Problems in Topology
- A partition calculus in set theory
- Introduction to Ramsey space
- Three chapters of measure theory in Isabelle/HOL
- Teilmengen von Mengen mit Relationen
- Combinatorial set theory: Partition relations for cardinals
- Title not available (Why is that?)
- The Jordan Curve Theorem, Formally and Informally
- Title not available (Why is that?)
- A partition theorem for the complete graph on \(\omega^\omega\)
- Pinning countable ordinals
- A short proof of a partition theorem for the ordinal ωω
- Countable partition ordinals
- A formal proof of the Kepler conjecture
- A Theorem in the Partition Calculus
- Analyzing Nash-Williams' partition theorem by means of ordinal types
- Title not available (Why is that?)
- The new Quickcheck for Isabelle. Random, exhaustive and symbolic testing under one roof
- Formalizing an analytic proof of the prime number theorem
- From LCF to Isabelle/HOL
- Tactics for mechanized reasoning: a commentary on Milner (1984) ‘The use of machines to assist in rigorous proof’
Cited In (8)
- Cardinals in Isabelle/HOL
- Towards formalising Schutz' axioms for Minkowski spacetime in Isabelle/HOL
- Formalizing calendars with the category of ordinals
- 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
- A formalised theorem in the partition calculus
- Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project
- Wetzel: formalisation of an undecidable problem linked to the continuum hypothesis
Uses Software
This page was built for publication: Formalizing ordinal partition relations using Isabelle/HOL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5094473)
