Representing and Searching the Space of Mathematical Knowledge
We discuss search in highly modular theory libraries. We represent such
libraries as OMDoc/MMT theory graphs and host them in the MathHub.info
system, a portal for active mathematical documents and an archive for
flexiformal mathematics. In theory graphs, statements can be inherited
(and thus need not be explicitly represented) via morphisms
that can include translations. This is good for knowledge management as
the number of induced (i.e. not explicitly represented) statements can grow
exponentially in the explicitly represented ones. But this is bad for
accessibility, since conventional (computer supported) access methods only
work on explicitly represented materials.
We claim that mathematicians are usually aware of the modular structure of the
mathematical domains they understand and induce the inherited knowledge space from the
documents they read and the discussions they participate in. In particular they conceive
mathematical domains as the induced knowledge space and can access it
independently of how it was represented in the sources. We call this access
pattern ``math-literate'', and observe that regular search engines for
mathematics (including our own MathWebSearch engine) are not, because they
cannot make the necessary coersions induced by theory morphisms.
In this paper we note that if the representation framework of the modular
library provides a systematic naming scheme for induced statements and the
library system implements a flattening operation that generates all induced
statements, then we can use this for access. We extend the MathWebSearch
System with index flattening and integrate it into MathHub.info as a
math-literate access system.