PRL Seminars
Progress on the ONR University Research Initiative in Digital Libraries for Computational Mathematics
December 2, 2001
Abstract
We discuss some of the most interesting results from the
participating members of the ONR URI on digital computational mathematics
libraries from the past four months. We focus on ideas for combining formal
and informal content in ways that enable rapid search in the on-line
Nuprl libraries using Google.
Cornell Work
Our research proposal stressed the value of connecting formal mathematics
to English language accountsof the same results. The most direct way to
start this study is through the use of the English summaries of proofs,
called glosses. Stuart Allen has provided these for many results in
elementary computational mathematics as part of an NSF project on formal
courseware.
We have studied how users access this material at our Web site, and we
discovered many connctions via Google. These examples led us to explore
the possibility of using Google as the entry point for search. Since we
have about 40K pages of mathematics on-line, Google indexes our material
deeply.
We explored this possibility by trying simple Google searches of the form:
Nuprl [math concept]. Some particular examples were:
| | Nuprl | Fibonacci |
| | Nuprl | Russell's paradox |
| | Nuprl | automata |
| | Nuprl | prime |
| | Nuprl | prime number |
| | Nuprl | square root |
We tried many more. The first item found is a Nuprl library page.
What is also remarkable is the number of articles and papers that show
up on the first Google page of ten items.
Stuart's Diagram:
Arrows show dependencies. The internal Google (dotted lines) is a
proposed new capability that we discussed in detail. We also
discussed the role of Amanda and Regina's work on natural language
generation.
|
|
|
|