### Abstract

This article defines the combinatorial structures known as Independence Systems and Matroids and provides basic concepts and theorems related to them. These structures play an important role in combinatorial optimisation, e. g. greedy algorithms such as Kruskal's algorithm. The development is based on Oxley's `What is a Matroid?'.

### License

BSD License

### Topics

- Mathematics/Combinatorics

### Session Matroids

- Indep_System
- Matroid

### Used by

- Kruskal’s Algorithm for Minimum Spanning Forest

## Cite

×

Matroids-AFP

    @article{Matroids-AFP,
      author  = {Jonas Keinholz},
      title   = {Matroids},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Matroids.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Nov 20, 2018 : Isabelle2018