Proof Pearl: A Probabilistic Proof for the Girth-Chromatic Number Theorem

1. Akbarpour, B., Paulson, L.C.: Metitarski: An automatic theorem prover for real-valued special functions. JAR 44, 175–205 (2010)

   Article  MathSciNet  MATH  Google Scholar 

2. Alon, N., Spencer, J.H.: The Probabilistic Method. Wiley (2000)

   Google Scholar 

3. Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in COQ. Science of Computer Programming 74(8), 568–589 (2009)

   Article  MathSciNet  MATH  Google Scholar 

4. Ballarin, C.: Interpretation of Locales in Isabelle: Theories and Proof Contexts. In: Borwein, J.M., Farmer, W.M. (eds.) MKM 2006. LNCS (LNAI), vol. 4108, pp. 31–43. Springer, Heidelberg (2006)

   Chapter  Google Scholar 

5. Bauer, G., Wenzel, M.T.: Calculational Reasoning Revisited (An Isabelle/Isar Experience). In: Boulton, R.J., Jackson, P.B. (eds.) TPHOLs 2001. LNCS, vol. 2152, pp. 75–90. Springer, Heidelberg (2001)

   Chapter  Google Scholar 

6. van Benthem, J.F.A.K., ter Meulen, A.G.: Generalized quantifiers in natural language. de Gruyter (1985)

   Google Scholar 

7. Bollobás, B.: Random Graphs. Academic Press (1985)

   Google Scholar 

8. Bourbaki, N.: General Topology (Part I). Addison-Wesley (1966)

   Google Scholar 

9. Butler, R.W., Sjogren, J.A.: A PVS graph theory library. Tech. rep., NASA Langley (1998)

   Google Scholar 

10. Chou, C.-T.: A Formal Theory of Undirected Graphs in Higher-Order Logic. In: Melham, T.F., Camilleri, J. (eds.) HUG 1994. LNCS, vol. 859, pp. 144–157. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

11. Diestel, R.: Graph Theory, GTM, 4th edn., vol. 173. Springer (2010)

    Google Scholar 

12. Endou, N., Narita, K., Shidama, Y.: The lebesgue monotone convergence theorem. Formalized Mathematics 16(2), 171–179 (2008)

    Article  Google Scholar 

13. Erdős, P., Rényi, A.: Asymmetric graphs. Acta Mathematica Hungarica 14, 295–315 (1963)

    Article  Google Scholar 

14. Erdős, P.: Graph theory and probability. Canad. J. Math. 11(11), 34–38 (1959)

    Article  MathSciNet  Google Scholar 

15. Erdős, P., Rényi, A.: On random graphs I. Publ. Math. Debrecen. 6, 290–297 (1959)

    MathSciNet  Google Scholar 

16. Gonthier, G.: A computer-checked proof of the Four Colour Theorem (2005)

    Google Scholar 

17. Hölzl, J., Heller, A.: Three Chapters of Measure Theory in Isabelle/HOL. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 135–151. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

18. Hurd, J.: Formal Verification of Probabilistic Algorithms. Ph.D. thesis, University of Cambridge (2002)

    Google Scholar 

19. Hurd, J.: Verification of the Miller-Rabin probabilistic primality test. JLAP 50(1-2), 3–21 (2003)

    Google Scholar 

20. Lee, G., Rudnicki, P.: Alternative graph structures. Formalized Mathematics 13(2), 235–252 (2005), Formal Proof Development

    Google Scholar 

21. Lester, D.R.: Topology in PVS: continuous mathematics with applications. In: Proc. AFM, pp. 11–20. ACM (2007)

    Google Scholar 

22. Lovász, L.: On chromatic number of finite set-systems. Acta Mathematica Hungarica 19, 59–67 (1968)

    Article  MATH  Google Scholar 

23. Mhamdi, T., Hasan, O., Tahar, S.: On the Formalization of the Lebesgue Integration Theory in HOL. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 387–402. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

24. Nipkow, T., Bauer, G., Schultz, P.: Flyspeck I: Tame Graphs. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 21–35. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

25. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002), http://isabelle.in.tum.de/dist/Isabelle2011-1/doc/tutorial.pdf

    MATH  Google Scholar 

26. Noschinski, L.: A probabilistic proof of the girth-chromatic number theorem. In: The Archive of Formal Proofs (February 2012), http://afp.sf.net/entries/Girth_Chromatic.shtml , Formal Proof Development

27. Rado, R.: Universal graphs and universal functions. Acta Arithmetica 9, 331–340 (1964)

    MathSciNet  MATH  Google Scholar 

28. Rudnicki, P., Stewart, L.: The Mycielskian of a graph. Formalized Mathematics 19(1), 27–34 (2011)

    Article  Google Scholar 

Download references