A Modular First Formalisation of Combinatorial Design Theory
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , |
|---|---|
| Format: | Preprint |
| Publié: |
2021
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866910287468167168 |
|---|---|
| author | Edmonds, Chelsea Paulson, Lawrence |
| author_facet | Edmonds, Chelsea Paulson, Lawrence |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2105_13583 |
| institution | arXiv |
| publishDate | 2021 |
| record_format | arxiv |
| spellingShingle | A Modular First Formalisation of Combinatorial Design Theory Edmonds, Chelsea Paulson, Lawrence Logic in Computer Science Combinatorics Logic 05B05, 68V20, 68V35, 03B35 F.4.1; G.2 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. |
| title | A Modular First Formalisation of Combinatorial Design Theory |
| topic | Logic in Computer Science Combinatorics Logic 05B05, 68V20, 68V35, 03B35 F.4.1; G.2 |
| url | https://arxiv.org/abs/2105.13583 |