A Formal Analysis of Algorithms for Matroids and Greedoids
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913916395716608 |
|---|---|
| author | Abdulaziz, Mohammad Ammer, Thomas Meenakshisundaram, Shriya Rimpapa, Adem |
| author_facet | Abdulaziz, Mohammad Ammer, Thomas Meenakshisundaram, Shriya Rimpapa, Adem |
| contents | We present a formal analysis, in Isabelle/HOL, of optimisation algorithms for matroids, which are useful generalisations of combinatorial structures that occur in optimisation, and greedoids, which are a generalisation of matroids. Although some formalisation work has been done earlier on matroids, our work here presents the first formalisation of results on greedoids, and many results we formalise in relation to matroids are also formalised for the first time in this work. We formalise the analysis of a number of optimisation algorithms for matroids and greedoids. We also derive from those algorithms executable implementations of Kruskal's algorithm for minimum spanning trees, an algorithm for maximum cardinality matching for bi-partite graphs, and Prim's algorithm for computing minimum weight spanning trees. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2505_19816 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Formal Analysis of Algorithms for Matroids and Greedoids Abdulaziz, Mohammad Ammer, Thomas Meenakshisundaram, Shriya Rimpapa, Adem Logic in Computer Science Data Structures and Algorithms Optimization and Control 68Qxx, 68Rxx, 68Wxx, 68V20, 90Bxx F.2.2; F.3.1; F.4.1 We present a formal analysis, in Isabelle/HOL, of optimisation algorithms for matroids, which are useful generalisations of combinatorial structures that occur in optimisation, and greedoids, which are a generalisation of matroids. Although some formalisation work has been done earlier on matroids, our work here presents the first formalisation of results on greedoids, and many results we formalise in relation to matroids are also formalised for the first time in this work. We formalise the analysis of a number of optimisation algorithms for matroids and greedoids. We also derive from those algorithms executable implementations of Kruskal's algorithm for minimum spanning trees, an algorithm for maximum cardinality matching for bi-partite graphs, and Prim's algorithm for computing minimum weight spanning trees. |
| title | A Formal Analysis of Algorithms for Matroids and Greedoids |
| topic | Logic in Computer Science Data Structures and Algorithms Optimization and Control 68Qxx, 68Rxx, 68Wxx, 68V20, 90Bxx F.2.2; F.3.1; F.4.1 |
| url | https://arxiv.org/abs/2505.19816 |