A modular first formalisation of combinatorial design theory

DOI10.1007/978-3-030-81097-9_1zbMath1485.68291arXiv2105.13583OpenAlexW3185338641MaRDI QIDQ2128787

Chelsea Edmonds, Lawrence Charles Paulson

Publication date: 22 April 2022

Full work available at URL: https://arxiv.org/abs/2105.13583

zbMATH Keywords

combinatoricslocalesblock designsIsabelle/HOLformalisationcombinatorial design theoryinteractive proof assistants

Mathematics Subject Classification ID

Frames, locales (06D22) Formalization of mathematics in connection with theorem provers (68V20) Designs and configurations (05Bxx)

Related Items

Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project ⋮ The formal verification of the ctm approach to forcing ⋮ Formalising Szemerédi's Regularity Lemma and Roth's Theorem on Arithmetic Progressions in Isabelle/HOL

Uses Software

• Isabelle
• MathScheme
• Graph Theory
• Archive Formal Proofs
• Latin Square
• Matroids

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A graph library for Isabelle
• Exploring the structure of an algebra text with locales
• Designs, Groups and Computing
• Constructive Type Classes in Isabelle
• Local Theory Specifications in Isabelle/Isar
• Combinatorial Designs
• Computational logic: its origins and applications
• Types for Proofs and Programs