Abstract
We describe two formal proofs of the finite version of Hall's Marriage Theorem performed with the proof assistant Isabelle/HOL, one by Halmos and Vaughan and one by Rado. The distinctive feature of our formalisation is that instead of sequences (often found in statements of this theorem) we employ indexed families, thus avoiding tedious reindexing of sequences. © 2011 Springer-Verlag.
Cite
CITATION STYLE
APA
Jiang, D., & Nipkow, T. (2011). Proof pearl: The marriage theorem. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7086 LNCS, pp. 394–399). https://doi.org/10.1007/978-3-642-25379-9_28
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
Already have an account? Sign in
Sign up for free