A modular first formalisation of combinatorial design theory

DOI10.1007/978-3-030-81097-9_1MaRDI QIDQ2128787zbMATHOpenAlexFDO

Authors Chelsea Edmonds, Lawrence C. Paulson

Publication date 22 April 2022

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

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)

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.

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

Cites work

• scientific article; zbMATH DE number 50655 (Why is no real title available?)
• scientific article; zbMATH DE number 1382770 (Why is no real title available?)
• A graph library for Isabelle
• Combinatorial Designs
• Computational logic: its origins and applications
• Constructive Type Classes in Isabelle
• Designs, groups and computing
• Exploring the structure of an algebra text with locales
• Local Theory Specifications in Isabelle/Isar
• The CRC handbook of combinatorial designs
• Tutorial to locales and locale interpretation
• Types for Proofs and Programs

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

Describes a project that uses

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)