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?'.
BibTeX:
@article{Matroids-AFP,
author = {Jonas Keinholz},
title = {Matroids},
journal = {Archive of Formal Proofs},
month = nov,
year = 2018,
note = {\url{https://isa-afp.org/entries/Matroids.html},
Formal proof development},
ISSN = {2150-914x},
}