A search engine for mathematical formulae

M Kohlhase, I Sucan - … conference on artificial intelligence and symbolic …, 2006 - Springer
International conference on artificial intelligence and symbolic computation, 2006Springer
We present a search engine for mathematical formulae. The MathWebSearch system
harvests the web for content representations (currently MathML and OpenMath) of formulae
and indexes them with substitution tree indexing, a technique originally developed for
accessing intermediate results in automated theorem provers. For querying, we present a
generic language extension approach that allows constructing queries by minimally
annotating existing representations. First experiments show that this architecture results in a …
Abstract
We present a search engine for mathematical formulae. The MathWebSearch system harvests the web for content representations (currently MathML and OpenMath) of formulae and indexes them with substitution tree indexing, a technique originally developed for accessing intermediate results in automated theorem provers. For querying, we present a generic language extension approach that allows constructing queries by minimally annotating existing representations. First experiments show that this architecture results in a scalable application.
Springer