TY - GEN
T1 - Proof pearl
T2 - 1st International Conference on Certified Programs and Proofs, CPP 2011
AU - Jiang, Dongchen
AU - Nipkow, Tobias
PY - 2011
Y1 - 2011
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=81855161332&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-25379-9_28
DO - 10.1007/978-3-642-25379-9_28
M3 - Conference contribution
AN - SCOPUS:81855161332
SN - 9783642253782
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 394
EP - 399
BT - Certified Programs and Proofs - First International Conference, CPP 2011, Proceedings
Y2 - 7 December 2011 through 9 December 2011
ER -