2026-07-21T19:26:06Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:24601 2025-12-12T15:09:48Z ddc:004 open_access

A Formal Analysis of Algorithms for Matroids and Greedoids Abdulaziz, Mohammad Ammer, Thomas Meenakshisundaram, Shriya Rimpapa, Adem Matroids Greedoids Combinatorial Optimisation Graph Algorithms Isabelle/HOL Formal Verification 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 computing optimal spanning trees, an algorithm for maximum cardinality matching for bi-partite graphs, and Prim’s algorithm for computing minimum weight spanning trees. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Mohammad Abdulaziz and Thomas Ammer and Shriya Meenakshisundaram and Adem Rimpapa 2025 Is Part Of LIPIcs, Volume 352, 16th International Conference on Interactive Theorem Proving (ITP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2025.2 urn:nbn:de:0030-drops-246012 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.2 eng https://creativecommons.org/licenses/by/4.0/legalcode