The MWS search engine is optimized for fast query responses and interactive applications. Unification queries form the basis for expressive query languages with well-defined semantics. Any corpus whose formulae can referenced by URIs and converted to Content MathML can be indexed by MWS.
The MWS search engine can be employed by various front-ends. Here are some web-based ones.
We are currently developing:
Our applications are largely restricted by our server capacities and in particular the RAM (we would like to offer a formula search engine for all of the arXiv.org, but would need another server with about 128GB RAM for that. If you want to donate server space or propose another application, contact Michael Kohlhase.