A formalised theorem in the partition calculus
From MaRDI portal
Publication:6073894
DOI10.1016/j.apal.2023.103246arXiv2104.11613OpenAlexW3157126958WikidataQ123365870 ScholiaQ123365870MaRDI QIDQ6073894
Publication date: 12 October 2023
Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2104.11613
Mechanization of proofs and logical operations (03B35) Partition relations (03E02) Ordinal and cardinal numbers (03E10) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (1)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Set theory. An introduction to independence proofs
- Nonconstructive computational mathematics
- The semantics of answer literals
- Isabelle/HOL. A proof assistant for higher-order logic
- The foundation of a generic theorem prover
- A term of length 4 523 659 424 929
- Single axioms for odd exponent groups
- A Ramsey theorem in Boyer-Moore logic
- From LCF to Isabelle/HOL
- Formalizing an analytic proof of the prime number theorem
- Partition Relations
- HOL Light: An Overview
- A Theorem in the Partition Calculus
- Negation in logic programming
- The Relative Consistency of the Axiom of Choice Mechanized Using Isabelle⁄zf
- Formalization of Forcing in Isabelle/ZF
- Formalizing Ordinal Partition Relations Using Isabelle/HOL
- Math Reviews® News
- A short proof of a partition theorem for the ordinal ωω
- A FORMAL PROOF OF THE KEPLER CONJECTURE
- A Machine-Checked Proof of the Odd Order Theorem
- A Machine-Oriented Logic Based on the Resolution Principle
- A Computing Procedure for Quantification Theory
This page was built for publication: A formalised theorem in the partition calculus
