### 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.

### License

BSD License

### Topics

- Mathematics/Combinatorics

### Session Design_Theory

- Multisets_Extras
- Design_Basics
- Design_Operations
- Block_Designs
- BIBD
- Resolvable_Designs
- Group_Divisible_Designs
- Designs_And_Graphs
- Sub_Designs
- Design_Isomorphisms
- Design_Theory_Root

### Depends on

- Cardinality of Set Partitions
- Graph Theory
- Formalization of Nested Multisets, Hereditary Multisets, and Syntactic Ordinals

### Used by

- General Probabilistic Techniques for Combinatorics and the Lovasz Local Lemma
- Hypergraphs
- Undirected Graph Theory
- Fisher’s Inequality: Linear Algebraic Proof Techniques for Combinatorics

### Auto-related entries

- Hypergraphs

## Cite

×

Design_Theory-AFP

    @article{Design_Theory-AFP,
      author  = {Chelsea Edmonds and Lawrence C. Paulson},
      title   = {Combinatorial Design Theory},
      journal = {Archive of Formal Proofs},
      month   = {August},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Design_Theory.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Sep 2, 2021 : Isabelle2021