Newer
Older
people:
- mkohlhase
- isucan
- cprodescu
- rhambasan
- ahambasan
---
The MathWebSearch system (MWS) is a content-based search engine for mathematical
formulae. It indexes MathML formulae, using a technique derived from automated theorem
proving: Substitution Tree Indexing. With this indexing technique MWS can answer
unification queries extremely efficiently (30-100 ms) on large sets of formulae (in the
Gigaformula range); but the index (up to 50GiB) needs to be kept in main memory.
MWS is the [formula search engine](https://zbmath.org/formulae/) employed in
[Zentralblatt Math](http://zbmath.org); see a
[demo on a mathematical subset](http://arxivsearch.mathweb.org) of the
[arXMLiv data set](/projects/arXMLiv/) [further demos](http://search.mathweb.org).