A Modular First Formalisation of Combinatorial Design Theory
Accepted version
Peer-reviewed
Repository URI
Repository DOI
Change log
Authors
Edmonds, C https://orcid.org/0000-0002-8559-9133
Paulson, LC https://orcid.org/0000-0003-0288-4279
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.
Description
Keywords
Isabelle/HOL, Combinatorics, Formalisation, Interactive proof assistants, Combinatorial design theory, Block designs, Locales
Journal Title
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Conference Name
Intelligent Computer Mathematics
Journal ISSN
0302-9743
1611-3349
1611-3349
Volume Title
12833 LNAI
Publisher
Springer International Publishing
Publisher DOI
Rights
All rights reserved
Sponsorship
European Research Council (742178)
ERC Advanced Grant ALEXANDRIA (Project GA 742178)