MBase: Representing knowledge and context for the integration of mathematical software systems. (English) Zbl 0981.68153

Summary: We describe the data model of the MBase system, a web-based, distributed mathematical knowledge base. This system is a mathematical service in MATHWEB that offers a universal repository of formalized mathematics where the formal representation allows semantics-based retrieval of distributed mathematical facts.
We classify the data necessary to represent mathematical knowledge and analyze its structure. For the logical formulation of mathematical concepts, we propose a methodology for developing representation formalisms for mathematical knowledge bases. We propose to concretely equip knowledge bases with a hierarchy of logical systems that are linked by logic morphisms. These mappings relativize formulae and proofs and thus support translation of the knowledge to the various formats currently in use in deduction systems. On the other hand they define higher language features from simpler ones and ultimately serve as a means to found the whole knowledge base in axiomatic set theory.
The viability of this approach is proven by developing a sorted record-\(\lambda\)-calculus with dependent sorts and labeled abstraction that is well-suited both for formalizing mathematical practice and supporting efficient inference services. This “mathematical vernacular” is an extension of a sorted \(\lambda\)-calculus by records, dependent record sorts and selection sorts.


68T30 Knowledge representation
Full Text: DOI


[1] Adams, A.; Gottliebsen, H.; Linton, S.; Martin, U., VSDITLU: A verifiable symbolic definite integral table look-up, (1999), p. 112-126 · Zbl 0943.68152
[2] Aı̈t-Kaci, H.; Garrigue, J., Label-selective lambda-calculus: syntax and confluence, Proceedings of the 13th international conference on foundations of software technology and theoretical computer science, (1993) · Zbl 0925.03090
[3] Andrews, P.B., An introduction to mathematical logic and type theory: to truth through proof, (1986), Academic Press Orlando · Zbl 0617.03001
[4] Andrews, P.B.; Bishop, M.; Issar, S.; Nesmith, D.; Pfenning, F.; Xi, H., TPS: a theorem-proving system for classical type theory, J. autom. reasoning, 16, 321-353, (1996) · Zbl 0858.03017
[5] Armando, A.; Kohlhase, M.; Ranise, S., Communication protocols for mathematical services based on KQML and OMRS, () · Zbl 0986.68003
[6] Autexier, S.; Hutter, D.; Mantel, H.; Schairer, A., Towards an evolutionary formal software-development using CASL, () · Zbl 0966.68140
[7] Ballarin, C.; Homann, K.; Calmet, J., Theorems and algorithms: an interface between isabelle and Maple, Proceedings of international symposium on symbolic and algebraic computation (ISSAC’95), (1995), ACM Press New York, p. 150-157 · Zbl 0922.68080
[8] Bauer, A.; Clarke, E.; Zhao, X., Analytica—an experiment in combining theorem proving and symbolic computation, J. autom. reasoning, 21, 295-325, (1998) · Zbl 0916.68143
[9] Benzmüller, C., ω mega: towards a mathematical assistant, (), 252-255
[10] Benzmüller, C.; Bishop, M.; Sorge, V., Integrating tps and ω mega, J. universal comput. sci., 5, (1999)
[11] Bishop, M.; Andrews, P.B., Selectively instantiating definitions, (1998), p. 365-380
[12] Boulton, R.; Slind, K.; Bundy, A.; Gordon, M., An interface between CLAM and HOL, (), 87-104
[13] T. Bray, J. Paoli, C. M. Sperberg-McQueen
[14] Calmet, J.; Homann, K., Towards a mathematics software bus, Theor. comput. sci., 107, (1997) · Zbl 0893.68036
[15] O. Caprotti, A. M. Cohen
[16] Cheikhrouhou, L.; Siekmann, J., Planning diagonalization proofs, (), 167-180 · Zbl 0929.03020
[17] Cohen, A.; Cuypers, H.; Sterk, H., Algebra interactive!, (1999), Springer Berlin
[18] de Bruijn, N.G., The mathematical vernacular, a language for mathematics with typed sets, (), 865-935
[19] S. Deach
[20] Ebbinghaus, H.D., Einführung in die mengenlehre, (1977), Wissenschaftliche Buchgesellschaft
[21] Farmer, W.M., Theory interpretation in simple type theory, HOA’93, an international workshop on higher-order algebra, logic and term rewriting, (1993), Springer Berlin
[22] Farmer, W.M.; Guttman, J.D.; Javier Thayer, F., IMPS: an interactive mathematical proof system, J. autom. reasoning, 11, 213-248, (October 1993)
[23] Finin, T.; Fritzson, R., KQML—a language and protocol for knowledge and information exchange, Proceedings of the 13th international distributed artificial intelligence workshop, Seattle, WA, U.S.A., (1994), p. 127-136
[24] Franke, A.; Hess, S.M.; Jung, C.G.; Kohlhase, M.; Sorge, V., Agent-oriented integration of distributed mathematical services, J. universal comput. sci., 5, 156-187, (1999) · Zbl 0961.68117
[25] A. Franke, M. Kohlhase, System description: MathWeb, an agent-based communication layer for distributed automated theorem proving, 217, 221
[26] Fraenkel, A.A., Zu den grundlagen der Cantor-zermeloschen mengenlehre, Math. annalen, 86, 230-237, (1922) · JFM 48.0199.04
[27] Ganzinger, H.ed., Proceedings of the 16th conference on automated deduction, LNAI 1632, (1999), Springer Berlin
[28] Gentzen, G., Untersuchungen über das logische schließen I & II, Math. Z., 39, 176, 210, 572.595, (1935) · Zbl 0010.14501
[29] Harrison, J.; Théry, L., A skeptic’s approach to combining HOL and Maple, J. autom. reasoning, 21, 279-294, (1998) · Zbl 0916.68142
[30] Hickey, J.J., Formal objects in type theory using very dependent types, Foundations of object oriented languages 3, (1996)
[31] Hindley, J.; Seldin, J., Introduction to combinators and lambda calculus, (1986), Cambridge University Press · Zbl 0614.03014
[32] Howe, D., Semantic foundations for embedding HOL in NUPRL, (), 85-101 · Zbl 0886.03008
[33] Huang, X.; Fiedler, A., presenting machine-found proofs, (1996), p. 221-225
[34] Hutter, D., reasoning about theories. technical report, deutsches forschungszentrum für Künstliche intelligenz (DFKI), (1999)
[35] Hutter, D.; Sengler, C., INKA—the next generation, (1996), p. 288-292
[36] P. Ion, R. Miner
[37] Kerber, M., How to prove higher order theorems in first order logic, (), 137-142 · Zbl 0746.68081
[38] Kerber, M.; Kohlhase, M.; Sorge, V., Integrating computer algebra into proof planning, J. autom. reasoning, 21, 327-355, (1998) · Zbl 0916.68144
[39] Kirchner, C.; Kirchner, H.eds., Proceedings of the 15th conference on automated deduction, (1998), Springer Berlin
[40] M. Kohlhase, 1994
[41] Kohlhase, M., omdoc: towards an Internet standard for the administration, distribution and teaching of mathematical knowledge, Proceedings AISC’2000, LNAI, (2000), Springer Berlin · Zbl 1042.00511
[42] Kohlhase, M., omdoc: towards an openmath representation of mathematical documents. seki report SR-00-02, fachbereich informatik, universität des saarlandes, (2001)
[43] Kohlhase, M.; Pfenning, F., Unification in a λ -calculus with intersection types, (), 488-505
[44] Language Design Task Group CoFI
[45] Loeckx, J.; Ehrig, H.-D.; Wolf, M., Specification of abstract data types, (1996), Teubner, Chichester New York
[46] McRobbie, M.A.; Slaney, J.K.eds., Proceedings of the 13th conference on automated deduction, (1996), Springer Berlin · Zbl 1102.68317
[47] Ohori, A., A polymorphic record calculus and its compilation, ACM trans. program. lang. syst., 17, 844-895, (1995)
[48] Paulson, L.C., Set theory for verification: I. from foundations to functions, J. autom. reasoning, 11, 353-389, (1993) · Zbl 0802.68128
[49] Quaife, A., Automated deduction in von neumann – bernays-Gödel set theory, J. autom. reasoning, 8, 91-148, (1992) · Zbl 0768.03005
[50] D. Raggett, A. L. Hors, I. Jacobs
[51] Richardson, J.D.C.; Smaill, A.; Green, I.M., system description: proof planning in higher-order logic with λclam, (1998)
[52] Siekmann, J., Adaptive course generation and presentation, ()
[53] Smolka, G., The oz programming model, (), 324-343
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.