A search engine for mathematical formulae. (English) Zbl 1156.68306

Kohlhase, Michael; Sucan, Ioan

Calmet, Jacques (ed.) et al., Artificial intelligence and symbolic computation. 8th international conference, AISC 2006, Beijing, China, September 20–22, 2006. Proceedings. Berlin: Springer (ISBN 978-3-540-39728-1/pbk). Lecture Notes in Computer Science 4120. Lecture Notes in Artificial Intelligence, 241-253 (2006).

Summary: 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.
For the entire collection see [Zbl 1149.68005].

MSC:

68M10	Network design and communication in computer systems
68P20	Information storage and retrieval of data
68T15	Theorem proving (deduction, resolution, etc.) (MSC2010)

Software:

OMDoc; Mathematica; MathWebSearch; MBase