
Fisher's
Inequality:
Linear
Algebraic
Proof
Techniques
for
Combinatorics
Title: 
Fisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics 
Authors:

Chelsea Edmonds and
Lawrence C. Paulson

Submission date: 
20220421 
Abstract: 
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
wellknown Fisher's inequality. We build on our prior work
formalising combinatorial design theory using a localecentric
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. 
BibTeX: 
@article{Fishers_InequalityAFP,
author = {Chelsea Edmonds and Lawrence C. Paulson},
title = {Fisher's Inequality: Linear Algebraic Proof Techniques for Combinatorics},
journal = {Archive of Formal Proofs},
month = apr,
year = 2022,
note = {\url{https://isaafp.org/entries/Fishers_Inequality.html},
Formal proof development},
ISSN = {2150914x},
}

License: 
BSD License 
Depends on: 
BenOr_Kozen_Reif, Berlekamp_Zassenhaus, Design_Theory, Groebner_Bases, ListIndex, Polynomial_Factorization 
Status: [ok] 
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.

