{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,3]],"date-time":"2024-09-03T20:41:44Z","timestamp":1725396104435},"reference-count":0,"publisher":"EasyChair","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We present fully formalized proofs of some central theorems from combinatorics. These are Dilworth's decomposition theorem, Mirsky's theorem, Hall's marriage theorem and the Erd\u0151s-Szekeres theorem. Dilworth's decomposition theorem is the key result among these. It states that in any finite partially ordered set (poset), the size of a smallest chain cover and a largest antichain are the same. Mirsky's theorem is a dual of Dilworth's decomposition theorem, which states that in any finite poset, the size of a smallest antichain cover and a largest chain are the same. We use Dilworth's theorem in the proofs of Hall's Marriage theorem and the Erd\u0151s-Szekeres theorem. The combinatorial objects involved in these theorems are sets and sequences. All the proofs are formalized in the Coq proof assistant. We develop a library of definitions and facts that can be used as a framework for formalizing other theorems on finite posets.<\/jats:p>","DOI":"10.29007\/r7fg","type":"proceedings-article","created":{"date-parts":[[2018,1,12]],"date-time":"2018-01-12T07:30:31Z","timestamp":1515742231000},"page":"43-27","source":"Crossref","is-referenced-by-count":0,"title":["Formalization of some central theorems in combinatorics of finite sets"],"prefix":"10.29007","volume":"1","author":[{"given":"Abhishek Kr","family":"Singh","sequence":"first","affiliation":[]}],"member":"11545","event":{"name":"IWIL Workshop and LPAR Short Presentations"},"container-title":["Kalpa Publications in Computing"],"original-title":[],"deposited":{"date-parts":[[2018,1,12]],"date-time":"2018-01-12T07:30:34Z","timestamp":1515742234000},"score":1,"resource":{"primary":{"URL":"https:\/\/easychair.org\/publications\/paper\/Nr"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"references-count":0,"URL":"https:\/\/doi.org\/10.29007\/r7fg","relation":{},"ISSN":["2515-1762"],"issn-type":[{"type":"print","value":"2515-1762"}],"subject":[]}}