| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Combinatorial Design Theory
| Title: | Combinatorial Design Theory |
| Authors: | Chelsea Edmonds and Lawrence Paulson |
| Submission date: | 2021-08-13 |
| Abstract: | Combinatorial design theory studies incidence set systems with certain balance and symmetry properties. It is closely related to hypergraph theory. This formalisation presents a general library for formal reasoning on incidence set systems, designs and their applications, including formal definitions and proofs for many key properties, operations, and theorems on the construction and existence of designs. Notably, this includes formalising t-designs, balanced incomplete block designs (BIBD), group divisible designs (GDD), pairwise balanced designs (PBD), design isomorphisms, and the relationship between graphs and designs. A locale-centric approach has been used to manage the relationships between the many different types of designs. Theorems of particular interest include the necessary conditions for existence of a BIBD, Wilson's construction on GDDs, and Bose's inequality on resolvable designs. Parts of this formalisation are explored in the paper "A Modular First Formalisation of Combinatorial Design Theory", presented at CICM 2021. |
| BibTeX: |
@article{Design_Theory-AFP,
author = {Chelsea Edmonds and Lawrence Paulson},
title = {Combinatorial Design Theory},
journal = {Archive of Formal Proofs},
month = aug,
year = 2021,
note = {\url{https://isa-afp.org/entries/Design_Theory.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | Card_Partitions, Graph_Theory, Nested_Multisets_Ordinals |
| Status: [failed] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |