KnowledgeBase » SEMINAR » ID = 568

Progress on the ONR University Research Initiative in Digital Libraries for Computational Mathematics

by Stuart F. Allen, Robert L. Constable
2001-2002

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.