We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Formalising Fisher's Inequality: Formal Linear Algebraic Proof Techniques in Combinatorics

Abstract: The formalisation of mathematics is continuing rapidly, however combinatorics continues to present challenges to formalisation efforts, such as its reliance on techniques from a wide range of other fields in mathematics. This paper presents formal linear algebraic techniques for proofs on incidence structures in Isabelle/HOL, and their application to the first formalisation of Fisher's inequality. In addition to formalising incidence matrices and simple techniques for reasoning on linear algebraic representations, the formalisation focuses on the linear algebra bound and rank arguments. These techniques can easily be adapted for future formalisations in combinatorics, as we demonstrate through further application to proofs of variations on Fisher's inequality.
Comments: Accepted to ITP 2022, to be published in conference proceedings
Subjects: Logic in Computer Science (cs.LO); Combinatorics (math.CO)
MSC classes: 68V20, 05B05, 05B20, 05D05
ACM classes: F.4.1; G.2
Cite as: arXiv:2207.02728 [cs.LO]
  (or arXiv:2207.02728v1 [cs.LO] for this version)

Submission history

From: Chelsea Edmonds Ms [view email]
[v1] Wed, 6 Jul 2022 14:55:11 GMT (237kb,D)

Link back to: arXiv, form interface, contact.