Virtual theories – A uniform interface to mathematical knowledge bases

Abstract

To support mathematical research, engineering, and education by computer systems, we need to deal with the differences between mathematical content collections and information systems available today. Unfortunately, these systems – ranging from Wikipedia to theorem prover libraries are usually only accessible via a dedicated web information system or a low-level API at the level of the raw database content. What we would want is a “programmatic, mathematical API” which would give access to the knowledge-bases programmatically via their mathematical constructions and properties. This paper takes a step into this direction by interpreting large knowledge bases as OMDoc/MMT theories – modular representations of mathematical objects and their properties. For this, we generalize OMDoc/MMT theories to “virtual theories” – theories so big that they do not fit into main memory – and update its knowledge management algorithms so that they can work directly with objects stored in external knowledge bases. An additional technical contribution is the introduction of a codec system that bridges between low-level encodings in databases and the abstract construction of mathematical objects.