A Search Engine for Mathematical Formulae

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.

• Type: Conference
• Year: 2006
• Where: AISC
• Authors: Michael Kohlhase, Ioan Sucan
• Keywords: AISC 2006, Artificial Intelligence, Automated Theorem Provers, Mathematical Formulae, Substitution Tree Indexing