Skip to content
Snippets Groups Projects
Commit 05f30304 authored by Michael Kohlhase's avatar Michael Kohlhase
Browse files

more

parent 20eb58a1
No related branches found
No related tags found
No related merge requests found
......@@ -21,4 +21,11 @@ publink: http://kwarc.github.io/bibs/mws
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.
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).
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment