Email Gateway (Apr 29 2022 at 17:24): Email Gateway (Apr 29 2022 at 17:24):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
I’d like to announce a new AFP entry.
Fisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics
by Chelsea Edmonds and Lawrence C. Paulson
Linear algebraic techniques are powerful, yet often underrated tools in
combinatorial proofs. This formalisation provides a library including matrix
representations of incidence set systems, general formal proof techniques for
the rank argument and linear bound argument, and finally a formalisation of a
number of variations of the well-known Fisher's inequality. We build on our
prior work formalising combinatorial design theory using a locale-centric
approach, including extensions such as constant intersect designs and dual
incidence systems. In addition to Fisher's inequality, we also formalise proofs
on other incidence system properties using the incidence matrix representation,
such as design existence, dual system relationships and incidence system
isomorphisms. This formalisation is presented in the paper "Formalising Fisher's
Inequality: Formal Linear Algebraic Techniques in Combinatorics", accepted to
ITP 2022.
https://www.isa-afp.org/entries/Fishers_Inequality.html
Enjoy,
René
Last updated: Jul 15 2022 at 23:21 UTC