[isabelle] New in the AFP: Combinatorial Design Theory

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.



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.