Computer Theorem Proving and HoTT

Downloads

Appel, K. and Haken, W. (1977a). Every Planar Map is Four Colorable Part I: Discharging. Illinois Journal of Mathematics Vol. 21, pp. 429–490. Appel, K., Haken, W. and Koch, J. (1977b). Every Planar Map is Four Colorable Part II: Reducibility. Illinois Journal of Mathematics Vol. 21, pp. 491–567. Banach, S. and Tarski, A. (1924). Sur la décomposition des ensembles de points en parties respectivement congruentes. Fundamenta Mathematicae Vol. 6, pp. 244–277. ISSN: 0016-2736(p) 1730-6329(e). Bauer, A. (2013a). The HoTT book: socio-technical aspects. http://math.andrej.com/2013/06/20/the-hott-book/. Bauer, A. (2013b). A video rendition of the collaboration on the HoTT book. http://vimeo.com/68761218. Frege, G. (1884). Die Grundlagen der Arithmetik. Breslau. Frege, G. (1893). Grundgesetze der Arithmetik, Vol. 1. Jena. GitHub (2013). A platform for collaborative projects. https://github.com/. Gödel, (1931). Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. Monatshefte für Mathematik und Physik 38: 173-98. Gonthier, G. (2008). Formal Proof – the Four-Color Theorem. Notices of the AMS, Vol. 55, No. 11, pp. 1382-1393. Gonthier (2013). Engineering Mathematics: The Odd Order Theorem Proof. Proceedings of POPL’13, pp. 1-2. Hurd, J. and Haworth, G. McC. (2010). Data assurance in opaque computations. Advances in Computer Games 12 (ed. H. J. van den Herik and P. Spronck), LNCS Vol. 6048. pp. 221-231. ISSN 0302-9743, ISBN 978-3-642-12992-6, doi 10.1007/978-3-642-12993-3_20. Lakatos, I. (1976). Proofs and Refutations: the Logic of Mathematical Discovery (ed. J. Worrall and E. Zahar). Cambridge University Press. ISBN 0-521-29038-4. Mackenzie, D. (2001). Mechanizing Proof. The MIT Press. ISBN 0-262-13393-8. Mann, A. (2003). A Case Study in Automated Theorem Proving: OTTER and EQP. Thesis, U. of Colorado. Mills, I. M., Mohr, P. J., Quinn, T. J., Taylor, B. N. and Williams, E. R. (2011). Adapting the International System of Units to the twenty-first century. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, Vol. 369, No. 1953, pp. 3907-3924. ISSN 1364-503X. doi: 10.1098/rsta.2011.0180. Newell, A., Shaw, J.C. and Simon, H.A. (1957). Empirical Explorations of the Logic Theory Machine: A Case study in Heuristic. Proceedings of the Western Joint Computer Conference, pp. 218-240, esp. p219. Shulman, G. (2013). The HoTT Book. http://golem.ph.utexas.edu/category/2013/06/the_hott_book.html. Sutcliffe, G. (2012). Report on Automated Theorem Proving and the ATP competition. The Alan Turing Centenary conference. http://videolectures.net/turing100_sutcliffe_theorem_competition/ esp. at 2ʹ 45ʺ. The Univalent Foundations Program, IAS (2013a). The official announcement of the HoTT book. http://homotopytypetheory.org/2013/06/20/the-hott-book/. The Univalent Foundations Program, IAS (2013b). Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book/. Whitehead, A.N. and Russell, B. (1910). Principia Mathematica, Vol. 1, esp. Chapter 2 and Theorem 2.01.