Skip to main content
Top
Published in: Journal of Automated Reasoning 2/2019

02-08-2018

Formalization of the Fundamental Group in Untyped Set Theory Using Auto2

Author: Bohua Zhan

Published in: Journal of Automated Reasoning | Issue 2/2019

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We present a new framework for formalizing mathematics in untyped set theory using auto2. We demonstrate that many difficulties with using set theory for formalization of mathematics can be addressed by improvements to automation, without sacrificing the inherent flexibility of the logic. As applications, we formalize in Isabelle/FOL the entire chain of development from the axioms of set theory to the definition of the fundamental group of an arbitrary topological space. The auto2 prover is used as the sole automation tool, and enables succinct proof scripts throughout the project.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Literature
2.
go back to reference Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formaliz. Reason. 9(1), 101–148 (2016)MathSciNet Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formaliz. Reason. 9(1), 101–148 (2016)MathSciNet
3.
go back to reference Bourbaki, N.: Theory of Sets. Springer, Berlin (2000) Bourbaki, N.: Theory of Sets. Springer, Berlin (2000)
5.
go back to reference Grabowski, A., Kornilowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formaliz. Reason. Spec. Issue: User Tutor. I 3(2), 153–245 (2010)MathSciNetMATH Grabowski, A., Kornilowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formaliz. Reason. Spec. Issue: User Tutor. I 3(2), 153–245 (2010)MathSciNetMATH
7.
go back to reference 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) 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.
go back to reference Kornilowicz, A., Shidama, Y., Grabowski, A.: The fundamental group. Formaliz. Math. 12(3), 261–268 (2004) Kornilowicz, A., Shidama, Y., Grabowski, A.: The fundamental group. Formaliz. Math. 12(3), 261–268 (2004)
9.
go back to reference 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) 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.
go back to reference 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) 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.
go back to reference 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) 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)
13.
go back to reference Moura, L., Bjourner, N.: Efficient E-matching for SMT Solvers. In: Automated Deduction, CADE-21, LNCS 4603, pp. 183–198 (2007) Moura, L., Bjourner, N.: Efficient E-matching for SMT Solvers. In: Automated Deduction, CADE-21, LNCS 4603, pp. 183–198 (2007)
14.
go back to reference Munkres, J.R.: Topology. Prentice Hall, Upper Saddle River (2000)MATH Munkres, J.R.: Topology. Prentice Hall, Upper Saddle River (2000)MATH
15.
17.
go back to reference Trybulec, A.: Some Features of the Mizar Language. In: ESPRIT Workshop (1993) Trybulec, A.: Some Features of the Mizar Language. In: ESPRIT Workshop (1993)
18.
go back to reference 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) 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.
go back to reference 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) 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)
Metadata
Title
Formalization of the Fundamental Group in Untyped Set Theory Using Auto2
Author
Bohua Zhan
Publication date
02-08-2018
Publisher
Springer Netherlands
Published in
Journal of Automated Reasoning / Issue 2/2019
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-018-9478-0

Other articles of this Issue 2/2019

Journal of Automated Reasoning 2/2019 Go to the issue

Premium Partner