A modular first formalisation of combinatorial design theory
From MaRDI portal
Publication:2128787
DOI10.1007/978-3-030-81097-9_1zbMATH Open1485.68291arXiv2105.13583OpenAlexW3185338641MaRDI QIDQ2128787FDOQ2128787
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
combinatoricslocalesIsabelle/HOLformalisationblock designscombinatorial design theoryinteractive proof assistants
Frames, locales (06D22) Formalization of mathematics in connection with theorem provers (68V20) Designs and configurations (05Bxx)
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Combinatorial Designs
- 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
- Exploring the structure of an algebra text with locales
- Computational logic: its origins and applications
Cited In (3)
Uses Software
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)
