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.