From 05f30304391dbbad94c86efdf97e57c45253dd26 Mon Sep 17 00:00:00 2001 From: Michael Kohlhase <michael.kohlhase@fau.de> Date: Tue, 3 Apr 2018 15:24:25 +0200 Subject: [PATCH] more --- systems/mws.md | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/systems/mws.md b/systems/mws.md index 77920cc..0d1c224 100644 --- a/systems/mws.md +++ b/systems/mws.md @@ -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). -- GitLab