Abstract:
The National Science Digital Library (NSDL) has the potential to transform science education
and research — it is an energizing conception inspired by experience with the Web and
our national belief in participatory science at all levels. The NSDL will bring depth to online
collections. It has the promise to be known for the authority of its content. In the case of the
mathematics collections, we propose ways to add considerable depth to mathematical texts,
significantly enhance the authority of the collections, and foster economical collaboration in
producing collections.
Mathematical and program text is unique because significant portions of it can be anchored
to counterparts in formal logical theories that are implemented by computer systems.
These systems check formal proofs for correctness, trace logical dependencies among assertions,
execute algorithms and other forms of computational content, and provide assistance
in symbolic manipulations of mathematical formulas and logical expressions. When elements
of expository text, such as definitions and theorems, are formally linked to their implemented
counterparts, we call the texts semantically anchored.
We have successfully experimented with semantically anchored mathematical documents
in education, scientific communication, and software documentation. We see significant
social and technical value in providing them in the NSDL. The research we propose will
leverage substantial investments made by governments, research laboratories, corporations,
and universities in creating large collections of computer-checked and interactively-generated
formal mathematics. The broad impact of our work is that it will make this research
investment accessible to a larger community and will turn this unique resource to educational
use.
We propose to extend common authoring tools (as opposed to formal proof development
tools) so that they can easily produce semantically anchored documents suitable for the
NSDL. These tools will enable authors to create these documents by drawing on a large collection
of already existing formal material. We propose to contribute sample documents to
the NSDL, and explore ways of promoting their use in education, documentation, scientific
communication, and research use. We believe that anchored documents will enable interconnected
collections where the computers support exact common reference among concepts
and thus greatly facilitate collaborative contributions to the NSDL. We will evaluate the
effectiveness of our authoring tools as we progress and monitor the formal collections to see
how they are used and how they can be improved for this purpose.
In the language of the program solicitation(NSF 03-530), the intellectual merit of our
work lies in solving technical problems associated with creating large-scale coherent collections
of authoritative mathematical texts. We propose a new method for using computers
to assure precise common reference among the texts, and provide economical means of authoring
semantically anchored texts and improving static text-based resources by anchoring
them. We also store formal metadata with the semantically anchored text.
Return
to Nuprl Page