arXiv Analytics

Sign in

arXiv:1703.06133 [cs.LO]AbstractReferencesReviewsResources

Fully Mechanized Proofs of Dilworths Theorem and Mirskys Theorem

Abhishek Kr Singh

Published 2017-03-17Version 1

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.

Related articles: Most relevant | Search more
arXiv:1505.05028 [cs.LO] (Published 2015-05-19)
Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant
arXiv:1803.01466 [cs.LO] (Published 2018-03-05)
Learning how to Prove: From the Coq Proof Assistant to Textbook Style
arXiv:cs/0510011 [cs.LO] (Published 2005-10-04)
Diophantus' 20th Problem and Fermat's Last Theorem for n=4: Formalization of Fermat's Proofs in the Coq Proof Assistant