A Modular First Formalisation of Combinatorial Design Theory
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.
Cite
@article{arxiv.2105.13583,
title = {A Modular First Formalisation of Combinatorial Design Theory},
author = {Chelsea Edmonds and Lawrence Paulson},
journal= {arXiv preprint arXiv:2105.13583},
year = {2024}
}
Comments
This paper has been accepted to CICM 2021. The full formalisation will be made available on the Isabelle AFP prior to the conference, and is alternatively available here: https://github.com/cledmonds/design-theory