A modular first formalisation of combinatorial design theory

DOI10.1007/978-3-030-81097-9_1zbMATH Open1485.68291arXiv2105.13583OpenAlexW3185338641MaRDI QIDQ2128787FDOQ2128787

Authors: Chelsea Edmonds, Lawrence C. Paulson 

Publication date: 22 April 2022

Abstract: Combinatorial design theory studies set systems with certain balance and symmetry properties and has applications to computer science and elsewhere. This paper presents a modular approach to formalising designs for the first time using Isabelle and assesses the usability of a locale-centric approach to formalisations of mathematical structures. We demonstrate how locales can be used to specify numerous types of designs and their hierarchy. The resulting library, which is concise and adaptable, includes formal definitions and proofs for many key properties, operations, and theorems on the construction and existence of designs.

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

Recommendations

• scientific article; zbMATH DE number 5139236
• A Modular Formalisation of Finite Group Theory
• Gröbner bases of modules and Faugère's \(F_4\) algorithm in Isabelle/HOL
• Publication:4944854
• scientific article; zbMATH DE number 3961622

zbMATH Keywords

combinatoricslocalesIsabelle/HOLformalisationblock designscombinatorial design theoryinteractive proof assistants

Mathematics Subject Classification ID

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

Cites Work

• Combinatorial Designs
• The CRC handbook of combinatorial designs
• Title not available (Why is that?)
• Title not available (Why is that?)
• Types for Proofs and Programs
• Constructive Type Classes in Isabelle
• Local Theory Specifications in Isabelle/Isar
• A graph library for Isabelle
• Designs, groups and computing
• Tutorial to locales and locale interpretation
• Exploring the structure of an algebra text with locales
• Computational logic: its origins and applications

Cited In (3)

• 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
• Large-scale formal proof for the working mathematician -- lessons learnt from the ALEXANDRIA project

Uses Software

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

This page was built for publication: A modular first formalisation of combinatorial design theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2128787)