Repository logo
 

A formalised theorem in the partition calculus

Accepted version
Peer-reviewed

Type

Article

Change log

Abstract

A paper on ordinal partitions by Erdős and Milner (1972) has been formalised using the proof assistant Isabelle/HOL, augmented with a library for Zermelo-Fraenkel set theory. The work is part of a project on formalising the partition calculus. The chosen material is particularly appropriate in view of the substantial corrections later published by its authors, illustrating the potential value of formal verification.

Description

Keywords

03E02, 03E05, 03E10, 03B35, 68V20, 68V35, math.LO, math.LO

Journal Title

Annals of Pure and Applied Logic

Conference Name

Journal ISSN

0168-0072

Volume Title

Publisher

Elsevier BV
Sponsorship
European Research Council (742178)
ERC Advanced Grant ALEXANDRIA (Project GA 742178)