Abstract
The problem of the integrity of a computer managed mathematical knowledge repository is in the heart of MKM since mathematical vernacular is a language permitting plenty of ways in expressing the same meaning. The users of the library are naturally forced to choose certain way among many similar ones, unless different approaches are provided by developers. Mizar is a system for formalizing mathematical content which is sufficient mature and flexible for a coexistence of different approaches of concrete subjects. Considering Mizar formalizations of ortholattice theory we discuss a useful mechanism of coping with the heterogeneity of theories in a library of mathematical facts.
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
Bancerek, G.: On the structure of Mizar types. In: Geuvers, H., Kamareddine, F. (eds.) Proc. of MLC 2003. ENTCS, vol. 85(7) (2003)
Bancerek, G.: Development of the theory of continuous lattices in Mizar. In: Kerber, M., Kohlhase, M. (eds.) Proceedings of the Symposium on Calculemus 2000, pp. 65–80 (2001)
Buchberger, B.: Mathematical Knowledge Management in Theorema. In: Buchberger, B., Caprotti, O. (eds.) Proceedings of MKM 2001, Linz, Austria (2001)
Constable, R.L.: Steps toward a World Wide Digital Library of Formal Mathematics. In: MKM Symposium, Edinburgh, UK (2003)
Cruz-Filipe, L., Geuvers, H., Wiedijk, F.: C-CoRN, the Constructive Coq Repository at Nijmegen, http://www.cs.kun.nl/~freek/notes/
Davenport, J.: Mathematical knowledge representation. In: Buchberger, B., Caprotti, O. (eds.) Proceedings of MKM 2001, Linz, Austria (2001)
Farmer, W., Guttman, J., Thayer, F.: Little theories. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 567–581. Springer, Heidelberg (1992)
Giuntini, R.: Quantum Logic and Hidden Variables, Bibliographisches Institute, Mannheim (1991)
Grabowski, A.: Robbins algebras vs. Boolean algebras. Formalized Mathematics 9(4), 681–690 (2001)
Grabowski, A., Moschner, M.: Formalization of ortholattices via orthoposets. Formalized Mathematics (to appear, 2004)
Grätzer, G.: General Lattice Theory. Academic Press, New York (1978)
Kozarkiewicz, V., Grabowski, A.: Axiomatization of lattices in terms of the Sheffer stroke. Formalized Mathematics (to appear, 2004)
McCune, W.: Solution of the Robbins problem. Journal of Automated Reasoning 19, 263–276 (1997)
The Mizar Home Page, http://mizar.org
Moschner, M.: Basic notions and properties of orthoposets. Formalized Mathematics 11(2), 201–210 (2003)
Nipkow, T., Paulson, L.C., Wenzel, M.T.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Prevosto, V., Jaume, M.: Making proofs in a hierarchy of mathematical structures. In: Hardin, T., Rioboo, R. (eds.) Proceedings of Calculemus 2003, Rome, Italy (2003)
Rudnicki, P., Trybulec, A.: Mathematical Knowledge Management in Mizar. In: Buchberger, B., Caprotti, O. (eds.) Proceedings of MKM 2001, Linz, Austria (2001)
Rudnicki, P., Trybulec, A.: On the integrity of a repository of formalized mathematics. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol. 2594, pp. 162–174. Springer, Heidelberg (2003)
Urban, J.: MPTP 0.1. In: Dahn, I., Vigneron, L. (eds.) Proc. of FTP 2003. ENTCS, vol. 86(1) (2003)
Wenzel, M.: Lattices and orders in Isabelle/HOL, http://isabelle.in.tum.de/library/HOL/Lattice
Wiedijk, F.: Formal proof sketches, http://www.cs.kun.nl/~freek/notes/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Grabowski, A., Moschner, M. (2004). Managing Heterogeneous Theories within a Mathematical Knowledge Repository. In: Asperti, A., Bancerek, G., Trybulec, A. (eds) Mathematical Knowledge Management. MKM 2004. Lecture Notes in Computer Science, vol 3119. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-27818-4_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-27818-4_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23029-8
Online ISBN: 978-3-540-27818-4
eBook Packages: Springer Book Archive