Abstract
In the paper we show, based on two problems in general topology (Kuratowski closure-complement and Isomichi’s classification of condensed subsets), how typed objects can be used instead of untyped text to better represent mathematical content understandable both for human and computer checker. We present mechanism of attributes and clusters reimplemented in Mizar fairly recently to fit authors’ expectations. The problem of knowledge reusability which is crucial if we develop a large unified repository of mathematical facts, is also addressed.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Journal of Formalized Mathematics, accessible at, http://mizar.uwb.edu.pl/JFM/ , Mizar library available at, ftp://mizar.uwb.edu.pl/pub/mml/
Bagińska, L.K., Grabowski, A.: On the Kuratowski closure-complement problem. Formalized Mathematics 11(3), 321–327 (2003); MML Id in [1]: KURAT0_1
Bancerek, G.: On the structure of Mizar types. In: Geuvers, H., Kamareddine, F. (eds.) Proc. of MLC 2003. ENTCS, vol. 85(7) (2003)
Cairns, P., Gow, J., Collins, P.: On dynamically presenting a topology course. Annals of Mathematics and Artificial Intelligence 38(1-3), 91–104 (2003)
Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-CoRN, the Constructive Coq Repository at Nijmegen. In: Asperti, A., Bancerek, G., Trybulec, A. (eds.) MKM 2004. LNCS, vol. 3119, pp. 88–103. Springer, Heidelberg (2004)
Darmochwał, A.: Families of subsets, subspaces and mappings in topological spaces. Formalized Mathematics 1(2), 257–261 (1990); MML Id in [1]: TOPS_2
Gierz, G., Hofmann, K.H., Keimel, K., Lawson, J.D., Mislove, M., Scott, D.S.: A Compendium of Continuous Lattices. Springer, Heidelberg (1980)
Isomichi, Y.: New concepts in the theory of topological space – supercondensed set, subcondensed set, and condensed set. Pacific Journal of Mathematics 38(3), 657–668 (1971)
Jastrzȩbska, M., Grabowski, A.: The properties of supercondensed sets, subcondensed sets, and condensed sets. To appear in Formalized Mathematics (2005); MML Id in [1]: ISOMICHI
Kelley, J.L.: General Topology. Van Nostrand (1955)
Kuratowski, K.: Sur l’opération \(\overline{A}\) de l’Analysis Situs. Fundamenta Mathematicae 3, 182–199 (1922)
Kuratowski, K.: Topology. PWN – Polish Scientific Publishers, Warszawa (1966)
Padlewska, B., Darmochwał, A.: Topological spaces and continuous functions. Formalized Mathematics 1(1), 223–230 (1990); MML Id in [1]: PRE_TOPC
Romanowicz, E., Grabowski, A.: Hall Marriage Theorem. Formalized Mathematics 12(3), 315–320 (2004); MML Id in [1]: HALLMAR1
Rusin, D.: Posting, available at, http://www.math.niu.edu/~rusin/known-math/94/kuratowski
Sambin, G.: Some points in formal topology. Theoretical Computer Science 305(1-3), 347–408 (2003)
Sherman, D.: Variations on Kuratowski’s 14-set theorem, available at, http://www.math.uiuc.edu/~dasherma/14-sets.pdf
Takeuchi, Y., Nakamura, Y.: On the Jordan curve theorem. Shinshu Univ. (1980)
Wiedijk, F.: Seventeen provers of the world, available at, http://www.cs.ru.nl/~freek/comparison/
Weisstein, E.W., et al.: Kuratowski’s closure-complement problem, from MathWorld – a Wolfram Web Resource, http://mathworld.wolfram.com/KuratowskisClosure-ComplementProblem.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Grabowski, A. (2006). Solving Two Problems in General Topology Via Types. In: Filliâtre, JC., Paulin-Mohring, C., Werner, B. (eds) Types for Proofs and Programs. TYPES 2004. Lecture Notes in Computer Science, vol 3839. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11617990_9
Download citation
DOI: https://doi.org/10.1007/11617990_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-31428-8
Online ISBN: 978-3-540-31429-5
eBook Packages: Computer ScienceComputer Science (R0)