Abstract: 
A matching in a graph G is a subset M of the
edges of G such that no two share an endpoint. A matching has maximum
cardinality if its cardinality is at least as large as that of any other
matching. An oddset cover OSC of a graph G is a
labeling of the nodes of G with integers such that every edge of
G is either incident to a node labeled 1 or connects two nodes
labeled with the same number i ≥ 2.
This article proves Edmonds theorem:
Let M be a matching in a graph G and let OSC be an
oddset cover of G.
For any i ≥ 0, let n(i) be the number of nodes
labeled i. If M = n(1) +
∑_{i ≥ 2}(n(i) div 2),
then M is a maximum cardinality matching.

BibTeX: 
@article{MaxCardMatchingAFP,
author = {Christine Rizkallah},
title = {Maximum Cardinality Matching},
journal = {Archive of Formal Proofs},
month = jul,
year = 2011,
note = {\url{http://isaafp.org/entries/MaxCardMatching.html},
Formal proof development},
ISSN = {2150914x},
}
