ITR: Formal Digital Library

Yale University, New Haven CT

Investigators

Abstract

CCR-ITR-0325808 ITR: Formal Digital Libraries Carsten Schuermann Mathematical 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.