MBase: Representing Knowledge and Context for the Integration of Mathematical Software Systems

In this article we describe the data model of the MB system, a web-based, distributed mathematical knowledge base. This system is a mathematical service in 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-λ -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λ -calculus by records, dependent record sorts and selection sorts.