Enabling Large-Scale Coherency Among Mathematical Texts in the NSDL

数学和程序代码文本是独一无二的，因为它的很大一部分可以与由计算机系统实现的形式逻辑理论中的对应部分相关联。这些系统检查形式证明的正确性，并跟踪断言之间的逻辑依赖关系。当说明性文本的元素，如定义和定理，正式地与其实现的对应元素相联系时，文本被称为“语义锚定的”。这类文本显示出相当的深度和权威性。这一有针对性的研究项目正在扩展通用的创作工具(相对于正式的校样开发工具)，以便它们能够轻松地生成适合国家科学数字图书馆(nsdl；http://nsdl.org).)的语义锚定的文档研究人员正在解决与创建权威数学文本的大规模连贯集合相关的技术问题；探索一种新的方法，利用计算机确保文本之间准确的共同参考；以及提供经济手段来创作语义锚定的文本，并通过锚定它们来改进基于静态文本的资源。由此产生的工具将使作者能够通过利用已有的和不断增长的形式材料的大量集合来创建语义锚定的文档。语义锚定的文档使相互关联的集合成为可能，其中计算机支持概念之间的精确公共引用。通过设计生成锚定文档的方法和工具，这项研究将极大地促进对NSDL的协作贡献。该项目正在向NSDL提供样本文件，并探索如何促进它们在教育、科学交流和研究中的使用。这项研究利用政府、研究实验室、公司和大学在创建大量计算机检查和交互生成的形式数学集合方面所做的大量投资。通过这个项目，与数学有关的作者、研究人员、学生和教师的广泛社区都可以访问这些收藏。

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.