Email Gateway (Sep 02 2021 at 12:42): Email Gateway (Sep 02 2021 at 12:42):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
I’m happy to announce the following new entry in the AFP.
Combinatorial Design Theory
by Chelsea Edmonds and Lawrence Paulson
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.
https://www.isa-afp.org/entries/Design_Theory.html
Enjoy,
René
Last updated: Apr 24 2024 at 20:16 UTC