A Modular First Formalisation of Combinatorial Design Theory

Chelsea Edmonds; Lawrence Paulson

REVIEW

Not yet reviewed by Pith; the record is open.

Re-run · record.json Download PDF Read on arXiv ↗

This paper has not been read by Pith yet. Machine review is queued; the pith claim, tier, and objections will appear here once it completes.

SPECIMEN: schema-true, not a live event

T0 review · schema-true

One-sentence machine reading of the paper's core claim.

pith:XXXXXXXX · record.json · timestamp

arxiv 2105.13583 v1 pith:G52EA66D submitted 2021-05-28 cs.LO math.COmath.LO

A Modular First Formalisation of Combinatorial Design Theory

Chelsea Edmonds , Lawrence Paulson This is my paper

classification cs.LO math.COmath.LO

keywords designsapproachcombinatorialdesignfirstmodularpropertiestheory

verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

0 comments

read the original abstract

Combinatorial design theory studies set systems with certain balance and symmetry properties and has applications to computer science and elsewhere. This paper presents a modular approach to formalising designs for the first time using Isabelle and assesses the usability of a locale-centric approach to formalisations of mathematical structures. We demonstrate how locales can be used to specify numerous types of designs and their hierarchy. The resulting library, which is concise and adaptable, includes formal definitions and proofs for many key properties, operations, and theorems on the construction and existence of designs.

A Modular First Formalisation of Combinatorial Design Theory

discussion (0)