{
"id": "1703.06133",
"version": "v1",
"published": "2017-03-17T17:55:35.000Z",
"updated": "2017-03-17T17:55:35.000Z",
"title": "Fully Mechanized Proofs of Dilworths Theorem and Mirskys Theorem",
"authors": [
"Abhishek Kr Singh"
],
"categories": [
"cs.LO",
"cs.DM"
],
"abstract": "We present two fully mechanized proofs of Dilworths and Mirskys theorems in the Coq proof assistant. Dilworths Theorem states that in any finite partially ordered set (poset), the size of a smallest chain cover and a largest antichain are the same. Mirskys Theorem is a dual of Dilworths Theorem. We formalize the proofs by Perles [2] (for Dilworths Theorem) and by Mirsky [5] (for the dual theorem). We also come up with a library of definitions and facts that can be used as a framework for formalizing other theorems on finite posets.",
"revisions": [
{
"version": "v1",
"updated": "2017-03-17T17:55:35.000Z"
}
],
"analyses": {
"keywords": [
"fully mechanized proofs",
"mirskys theorem",
"dilworths theorem states",
"smallest chain cover",
"coq proof assistant"
],
"note": {
"typesetting": "TeX",
"pages": 0,
"language": "en",
"license": "arXiv",
"status": "editable"
}
}
}