MBase
MBase: Representing Knowledge and Context for the Integration of Mathematical Software Systems. 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-λ-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.
Keywords for this software
References in zbMATH (referenced in 16 articles )
Showing results 1 to 16 of 16.
Sorted by year (- Kohlhase, Michael; Sucan, Ioan: A search engine for mathematical formulae (2006)
- Siekmann, Jörg; Benzmüller, Christoph; Autexier, Serge: Computer supported mathematics with $\Omega$MEGA (2006)
- Benzmüller, Christoph; Meier, Andreas; Sorge, Volker: Bridging theorem proving and mathematical knowledge retrieval (2005)
- Siekmann, Jörg; Benzmüller, Christoph: $\Omega$MEGA: Computer supported mathematics (2004)
- Kohlhase, Michael; Anghelache, Romeo: Towards collaborative content management and version control for structured mathematical knowledge (2003)
- Sacerdoti Coen, Claudio: From proof-assistants to distributed libraries of mathematics: Tips and pitfalls (2003)
- Siekmann, Jörg; Benzmüller, Christoph; Fiedler, Armin; Meier, Andreas; Normann, Immanuel; Pollet, Martin: Proof development with $\Omega$MEGA: the irrationality of $\sqrt 2$ (2003)
- Melham, T. F.: PROSPER. An investigation into software architecture for embedded proof engines (2002)
- Siekmann, J.; Benzmüller, C.; Fiedler, A.; Meier, A.; Pollet, M.: Proof development with $\Omega$MEGA: $\sqrt2$ is irrational (2002)
- Benzmüller, Christoph; Meier, Andreas; Sorge, Volker: Distributed assertion retrieval (2001)
- Caprotti, O.; Cohen, A. M.: On the role of OpenMath in interactive mathematical documents (2001)
- Kohlhase, Michael: OMDOC: Towards an internet standard for the administration, distribution, and teaching of mathematical knowledge (2001)
- Kohlhase, Michael; Franke, Andreas: MBase: Representing knowledge and context for the integration of mathematical software systems (2001)
- Voronkov, Andrei: Algorithms, datastructures, and other issues in efficient automated deduction (2001)
- Franke, Andreas; Kohlhase, Michael: System description: MBase, an open mathematical knowledge base (2000)
- Franke, Andreas; Kohlhase, Michael: MBase: Representing mathematical knowledge in a relational data base (1999)