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

Kohlhase, Michael; Franke, Andreas

J. Symb. Comput. 32, No. 4, 365-402 (2001).

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.

MSC:

68T30

Knowledge representation

Keywords:

MBase system; knowledge base

Software:

InKa; VSDITLU; Isabelle/ZF; ETPS; Automath; Lambda-Clam; MBase; OMDoc; Oz; Analytica; OMRS; PROVERB; IMPS; KQML; TPS

References:

[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: 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, (Kerber, M.; Kohlhase, M., CALCULEMUS-2000, Systems for Integrated Computation and Deduction (2001), St. Andrews, AKPeters, Natick: St. Andrews, AKPeters, Natick Scotland) · Zbl 0986.68003
[6]	Autexier, S.; Hutter, D.; Mantel, H.; Schairer, A., Towards an evolutionary formal software-development using CASL, (Choppy, C.; Bert, D., Proceedings Workshop on Algebraic Development Techniques, WADT-99 (2000), Springer: Springer Berlin) · 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: 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, (McCune, W., Proceedings of the 14th Conference on Automated Deduction (1997), Springer: Springer Berlin), 252-255 · Zbl 1430.68393
[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, (Grundy, J.; Newey, M., Theorem Proving in Higher Order Logics: Emerging Trends (1998), The Australian National University: The Australian National University Canberra), 87-104
[13]	T. Bray, J. Paoli, C. M. Sperberg-McQueen; 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; O. Caprotti, A. M. Cohen
[16]	Cheikhrouhou, L.; Siekmann, J., Planning diagonalization proofs, (Giunchiglia, F., Artificial Intelligence: Methodology, Systems and Applications (1998), Springer: Springer Berlin), 167-180 · Zbl 0929.03020
[17]	Cohen, A.; Cuypers, H.; Sterk, H., Algebra Interactive! (1999), Springer: Springer Berlin · Zbl 0940.00001
[18]	de Bruijn, N. G., The mathematical vernacular, a language for mathematics with typed sets, (Nederpelt, R. P.; Geuvers, J. H.; de Vrijer, R. C., Selected Papers on Automath (1994), Elsevier: Elsevier Amsterdam), 865-935
[19]	S. Deach; S. Deach
[20]	Ebbinghaus, H. D., Einführung in die Mengenlehre (1977), Wissenschaftliche Buchgesellschaft · Zbl 0357.04002
[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: 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) · Zbl 0802.68129
[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; A. Franke, M. Kohlhase, System description: MathWeb, an agent-based communication layer for distributed automated theorem proving
[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: Springer Berlin · Zbl 0917.00015
[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, (Wirsing, M.; Nivat, M., Algebraic Methodolgy and Software Technology (1996), Springer: Springer Berlin), 85-101 · Zbl 0886.03008
[33]	Huang, X.; Fiedler, A., Presenting machine-found proofs (1996), p. 221-225 · Zbl 1412.68235
[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 · Zbl 1412.68236
[36]	P. Ion, R. Miner; P. Ion, R. Miner
[37]	Kerber, M., How to prove higher order theorems in first order logic, (Mylopoulos, J.; Reiter, R., Proceedings IJCAI’91 (1991), Morgan Kaufmann: Morgan Kaufmann San Francisco), 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: Springer Berlin · Zbl 0892.00047
[40]	M. Kohlhase, 1994; 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: 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, (Miller, D., Proceedings of the International Logic Programming Sympsion, ILPS’93 (1993), MIT Press: MIT Press Cambridge MA), 488-505
[44]	Language Design Task Group CoFI; Language Design Task Group CoFI
[45]	Loeckx, J.; Ehrig, H.-D.; Wolf, M., Specification of Abstract Data Types (1996), Teubner, Chichester: Teubner, Chichester New York · Zbl 0868.68077
[46]	McRobbie, M. A.; Slaney, J. K.eds., Proceedings of the 13th Conference on Automated Deduction (1996), Springer: 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; 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, (Brusilovski, P., Proceedings of ITS-2000 Workshop on Adaptive and Intelligent Web-Based Education Systems (2000), Montreal)
[53]	Smolka, G., The Oz programming model, (van Leeuwen, J., Computer Science Today (1995), Springer: Springer Berlin), 324-343