Formalization of the Fundamental Group in Untyped Set Theory Using Auto2

1. Arthan, R.D.: Some Mathematical Case Studies in ProofPower-HOL. https://www.lemma-one.com/papers/51.pdf. Accessed 22 July 2018

2. Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formaliz. Reason. 9(1), 101–148 (2016)

   MathSciNet  Google Scholar 

3. Bourbaki, N.: Theory of Sets. Springer, Berlin (2000)

   Google Scholar 

4. Brunerie, G.: On the homotopy groups of spheres in homotopy type theory. Ph.D. Thesis. https://arxiv.org/abs/1606.05916

5. Grabowski, A., Kornilowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formaliz. Reason. Spec. Issue: User Tutor. I 3(2), 153–245 (2010)

   MathSciNet  MATH  Google Scholar 

6. IsarMathLib: http://www.nongnu.org/isarmathlib/

7. Kaliszyk C., Pak, K., and Urban, J.: Towards a Mizar environment for Isabelle: foundations and language. In: Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2016), ACM, New York, NY, USA, pp. 58–65 (2016)

8. Kornilowicz, A., Shidama, Y., Grabowski, A.: The fundamental group. Formaliz. Math. 12(3), 261–268 (2004)

   Google Scholar 

9. Kuncar, O.: Reconstruction of the Mizar type system in the HOL Light system. In: Pavlu, J., Safrankova, J. (eds.) WDS Proceedings of Contributed Papers: Part I—Mathematics and Computer Sciences, pp. 7–12. Matfyzpress (2010)

10. Lee, G., Rudnicki, P.: Alternative Aggregates in Mizar. In: Kauers M., Kerber M., Miner R., Windsteiger W. (eds) Towards mechanized mathematical assistants. LNCS, vol 4573, Springer, Berlin (2007)

11. Mahboubi, A., Tassi, E.: Canonical Structures for the Working Coq User. In: Blazy S., Paulin-Mohring C., Pichardie D. (eds.) ITP 2013. LNCS, vol 7998, Springer, Berlin, pp. 19–34 (2013)

12. Megill, N.D.: Metamath: A computer language for pure mathematics. http://us.metamath.org/downloads/metamath.pdf. Accessed 22 July 2018

13. Moura, L., Bjourner, N.: Efficient E-matching for SMT Solvers. In: Automated Deduction, CADE-21, LNCS 4603, pp. 183–198 (2007)

14. Munkres, J.R.: Topology. Prentice Hall, Upper Saddle River (2000)

    MATH  Google Scholar 

15. Paulson, L.C.: Set theory for verification: I. From foundations to functions. J. Autom. Reason. 11(3), 353–389 (1993)

    Article  MathSciNet  MATH  Google Scholar 

16. Paulson, L.C.: Set theory for verification: II. Induction and recursion. J. Autom. Reason. 15(2), 167–215 (1995)

    Article  MathSciNet  MATH  Google Scholar 

17. Trybulec, A.: Some Features of the Mizar Language. In: ESPRIT Workshop (1993)

18. Wiedijk, F.: Mizar’s Soft Type System. In: Schneider K., Brandt J. (eds.) Theorem Proving in Higher Order Logics, LNCS, vol 4732, Springer, Berlin (2007)

19. Zhan, B.: AUTO2: a saturation-based heuristic prover for higher-order logic. In: Blanchette, J.C., Merz, S. (eds.): ITP 2016, LNCS 9807, pp. 441–456 (2016)

Download references