Enabling Large-Scale Coherency Among Mathematical Texts in the NSDL

Cornell University, Ithaca NY

Investigators

Abstract

Mathematical and program-code 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 and trace logical dependencies among assertions. When elements of expository text, such as definitions and theorems, are formally linked to their implemented counterparts, the texts are said to be "semantically anchored." Such texts exhibit considerable depth and authority. This Targeted Research project is extending common authoring tools (text editors, as opposed to formal proof development tools) so that they can easily produce semantically anchored documents suitable for the National Science Digital Library (NSDL; http://nsdl.org). The investigators are solving technical problems associated with creating large-scale coherent collections of authoritative mathematical texts; exploring a new method for using computers to assure precise common reference among the texts; and providing economical means of authoring semantically anchored texts and improving static text-based resources by anchoring them. The resulting tools will enable authors to create semantically anchored documents by drawing on a large, already existing and growing, collection of formal material. Semantically anchored documents enable interconnected collections, where the computers support exact common reference among concepts. By designing methods and tools for generating anchored documents, this research will greatly facilitate collaborative contributions to the NSDL. The project is contributing sample documents to the NSDL and exploring ways of promoting their use in education, scientific communication, and research. This research leverages substantial investments made by governments, research laboratories, corporations, and universities in creating large collections of computer-checked and interactively generated formal mathematics. Through this project, these collections are being made accessible to an extended community of authors, researchers, students, and teachers involved with mathematics.