×

Semantic representation of general topology in the Wolfram language. (English) Zbl 1367.68303

Geuvers, Herman (ed.) et al., Intelligent computer mathematics. 10th international conference, CICM 2017, Edinburgh, UK, July 17–21, 2017. Proceedings. Cham: Springer (ISBN 978-3-319-62074-9/pbk; 978-3-319-62075-6/ebook). Lecture Notes in Computer Science 10383. Lecture Notes in Artificial Intelligence, 163-177 (2017).
Summary: The Wolfram Knowledgebase, powered by the entity framework, contains expertly curated data from thousands of diverse domains. We have begun expanding this framework to include mathematical knowledge, making significant strides in the representation of results pertaining to continued fractions, function spaces, and most recently, topology. This paper will focus on our progress in the representation of general topology. We have curated over 700 entities representing concept definitions, theorem statements, and concrete topological spaces, as well as their corresponding properties, including their formal representations as well as references, computed properties, and other metadata. Virtually every formal representation in this project required extensions to the Wolfram Language, mostly for basic set theory. We will outline all of these design choices by way of examples, as well as present additional functionality for querying, usage messages, formatting, and other computations.
For the entire collection see [Zbl 1364.68010].

MSC:

68T30 Knowledge representation
54-XX General topology
68W30 Symbolic computation and algebraic computation
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Bancerek, G., Byliński, C., Grabowski, A., Korniłowicz, A., Matuszewski, R., Naumowicz, A., Pąk, K., Urban, J.: Mizar: state-of-the-art and beyond. In: Kerber, M., Carette, J., Kaliszyk, C., Rabe, F., Sorge, V. (eds.) CICM 2015. LNCS, vol. 9150, pp. 261–279. Springer, Cham (2015). doi: 10.1007/978-3-319-20615-8_17 · Zbl 1417.68201 · doi:10.1007/978-3-319-20615-8_17
[2] Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-662-07964-5 · Zbl 1069.68095
[3] Dabbs, J.: \[ \pi \]
-Base. https://topology.jdabbs.com/
[4] Harrison, J.: HOL light: a tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265–269. Springer, Heidelberg (1996). doi: 10.1007/BFb0031814 · doi:10.1007/BFb0031814
[5] Iancu, M.: Towards Flexiformal Mathematics. Ph.D. thesis, Jacobs University (2016)
[6] Kieffer, S., Avigad, J., Friedman, H.: A language for mathematical knowledge management, January 2011. https://arxiv.org/abs/0805.1386
[7] Lewis, R.Y.: An extensible ad hoc interface between Lean and Mathematica. http://www.andrew.cmu.edu/user/rlewis1/leanmm/leanmm_public_draft.pdf
[8] Megill, N.: Metamath: A Computer Language for Pure Mathematics. Lulu Press, Morrisville
[9] de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The Lean Theorem Prover (system description). https://leanprover.github.io/papers/system.pdf · Zbl 1465.68279
[10] Munkres, J.: Topology, 2nd edn. Prentice Hall, Upper Saddle River (2000)
[11] Nipkow, T., Klein, G.: Concrete Semantics - With Isabelle/HOL. Springer, Cham (2014). http://dx.doi.org/10.1007/978-3-319-10542-0 · Zbl 1410.68004
[12] Steen, L., Seebach, J.A.: Counterexamples in Topology, 2nd edn. Springer, New York (1978) · Zbl 0386.54001 · doi:10.1007/978-1-4612-6290-9
[13] Wolfram Research Inc.: Wolfram Data Repository. https://datarepository.wolframcloud.com/
[14] Wolfram Research Inc.: Wolfram Knowledgebase. https://www.wolfram.com/knowledgebase/
[15] Wolfram Research Inc.: The Wolfram Language. https://www.wolfram.com/language/
[16] Wolfram Research Inc.: Wolfram Language & System Documentation Center. Assumptions and Domains. http://reference.wolfram.com/language/guide/AssumptionsAndDomains.html
[17] Wolfram Research Inc.: Wolfram Language & System Documentation Center. Expressions. https://reference.wolfram.com/language/tutorial/ExpressionsOverview.html
[18] Wolfram Research Inc.: Wolfram Language & System Documentation Center. Knowledge Representation & Access. https://reference.wolfram.com/language/guide/KnowledgeRepresentationAndAccess.html
[19] Wolfram Research Inc.: Wolfram Language & System Documentation. Logic & Boolean Algebra. https://reference.wolfram.com/language/guide/LogicAndBooleanAlgebra.html
[20] Wolfram Research Inc.: Wolfram
\[ | \]
Alpha. https://www.wolframalpha.com/
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.