ITR: Formal Digital Library

CCR-ITR-0325808 ITR：正式的数字图书馆Carsten Schuermann数学知识是科学和工程的核心。 数学知识的数量增长速度超过了我们形式化和组织数学知识的能力，本文的研究重点是开发形式化数字图书馆（FDL），一个用于管理和共享数学知识和形式化证明的公共和开放的基础设施。 这项工作的核心是设计一个逻辑框架，作为逻辑形式主义，个别理论和证明的表示语言，与定理证明系统，如PVS或HOL，在工业实践中一直有效的接口。 FDL强调定理证明系统之间的互操作性，以及不同系统之间数学事实的交换和重用。 FDL基础设施的设计是可扩展的知识库的大小以及形式主义的多样性。FDL项目鼓励工业界和学术界贡献，维护和使用与硬件，软件和工程中的形式化方法相关的基本数学知识。 FDL项目通过以易于使用的形式正式化和组织实用数学知识，为网络基础设施做出了贡献。FDL的应用领域包括教育、计算机辅助设计、数学建模、形式验证和科学研究。

CCR-ITR-0325808ITR: Formal Digital LibrariesCarsten SchuermannMathematical knowledge is at the core of science and engineering. The quantity of mathematical knowledge is growing faster than our ability to formalize and organize it. The proposed research focuses on developing Formal Digital Libraries (FDL), a common and open infrastructure for managing and sharing mathematical knowledge and formal proof. Central to this work is the design of a logical framework as a representation language for logical formalisms, individual theories, and proofs, with an interface to theorem proving systems such as PVS or HOL, that have been effective in industrial practice. FDL emphasizes interoperability between theorem proving systems, and the exchange and reusability of mathematical facts across different systems. The FDL infrastructure is designed to be scalable with respect to the size of the knowledge base as well as the diversity of formalisms.The FDL project encourages industry and academia to contribute, maintain, and use basic mathematical knowledge related to formal methods in hardware, software, and engineering. The FDL project contributes to the cyberinfrastructure by formalizing and organizing practical mathematical knowledge in a readily usable form. Application areas for FDL include education, computer-aided design, mathematical modelling, formal verification, and scientific research.