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

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].


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