Abstract
Since there are different ways of axiomatizing and developing a mathematical theory, knowledge about a such a theory may reside in many places and in many forms within a library of formalized mathematics. We introduce the notion of a realm as a structure for consolidating knowledge about a mathematical theory. A realm contains several axiomatizations of a theory that are separately developed. Views interconnect these developments and establish that the axiomatizations are equivalent in the sense of being mutually interpretable. A realm also contains an external interface that is convenient for users of the library who want to apply the concepts and facts of the theory without delving into the details of how the concepts and facts were developed. We illustrate the utility of realms through a series of examples. We also give an outline of the mechanisms that are needed to create and maintain realms.
This is a preview of subscription content, log in via an institution to check access.
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
Carette, J., Farmer, W.M.: High-Level Theories. In: Autexier, S., Campbell, J., Rubio, J., Sorge, V., Suzuki, M., Wiedijk, F. (eds.) AISC/Calculemus/MKM 2008. LNCS (LNAI), vol. 5144, pp. 232–245. Springer, Heidelberg (2008)
Carette, J., Farmer, W.M., O’Connor, R.: MathScheme: Project description. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) Calculemus/MKM 2011. LNCS (LNAI), vol. 6824, pp. 287–288. Springer, Heidelberg (2011)
Carette, J., O’Connor, R.: Theory Presentation Combinators. In: Jeuring, J., Campbell, J.A., Carette, J., Dos Reis, G., Sojka, P., Wenzel, M., Sorge, V. (eds.) CICM 2012. LNCS (LNAI), vol. 7362, pp. 202–215. Springer, Heidelberg (2012)
Farmer, W.M.: Biform Theories in Chiron. In: Kauers, M., Kerber, M., Miner, R., Windsteiger, W. (eds.) MKM/Calculemus 2007. LNCS (LNAI), vol. 4573, pp. 66–79. Springer, Heidelberg (2007)
Farmer, W.M.: Mathematical Knowledge Management. In: Schwartz, D., Te’eni, D. (eds.) Encyclopedia of Knowledge Management, 2nd edn., pp. 1082–1089. Idea Group Reference (2011)
Farmer, W.M., Guttman, J.D., Thayer, F.J.: Little Theories. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 567–581. Springer, Heidelberg (1992)
Halleck, J.: http://home.utah.edu/~nahaj/logic/structures/systems/s4.html (accessed: March 14, 2014)
Hall, M.: The Theory of Groups. The Macmillan Company, New York (1959)
Kohlhase, M., Iancu, M.: Searching the Space of Mathematical Knowledge. In: Sojka, P., Kohlhase, M. (eds.) DML and MIR 2012. Masaryk University, Brno (2012) (in press) ISBN: 978-80-210-5542-1
Kargapolov, M.I., Merzljakov, J.I.: Fundamentals of the Theory of Groups. Graduate Texts in Mathematics. Springer (1979)
Kohlhase, M., Rabe, F., Zholudev, V.: Towards MKM in the Large: Modular Representation and Scalable Software Architecture. In: Autexier, S., Calmet, J., Delahaye, D., Ion, P.D.F., Rideau, L., Rioboo, R., Sexton, A.P. (eds.) AISC/Calculemus/MKM 2010. LNCS (LNAI), vol. 6167, pp. 370–384. Springer, Heidelberg (2010), arXiv:1005.5232v2 [cs.OH]
Lawvere, W.F.: Functorial Semantics of Algebraic Theories. Reprints in Theory and Applications of Categories 4, 1–121 (2004)
Lack, S., Rosický, J.: Notions of Lawvere Theory. English. Applied Categorical Structures 19(1), 363–391 (2011), doi:10.1007/s10485-009-9215-2, ISSN: 0927-2852
Rabe, F.: The MMT Language and System, https://svn.kwarc.info/repos/MMT (visited on November 10, 2011)
Peano, G.: Arithmetices principia nova methodo exposita. Bocca, Turin (1889)
Rabe, F., Kohlhase, M.: A Scalable Module System. Information & Computation (230), 1–54 (2013)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Carette, J., Farmer, W.M., Kohlhase, M. (2014). Realms: A Structure for Consolidating Knowledge about Mathematical Theories. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds) Intelligent Computer Mathematics. CICM 2014. Lecture Notes in Computer Science(), vol 8543. Springer, Cham. https://doi.org/10.1007/978-3-319-08434-3_19
Download citation
DOI: https://doi.org/10.1007/978-3-319-08434-3_19
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-08433-6
Online ISBN: 978-3-319-08434-3
eBook Packages: Computer ScienceComputer Science (R0)