FDL: A Prototype Formal Digital Library

This manual describes the first prototype of a new kind of system which we call a Formal Digital Library (FDL). We designed the system and assembled the prototype as part of a research project sponsored by the Office of Naval Research entitled Building Interactive Digital Libraries of Formal Algorithmic Knowledge. A key purpose of the prototype library is to demonstrate that it is possible to build a system with many of the properties called for in the project proposal and to illustrate important scenarios for its use. Experience with the prototype library will influence the design and construction of an improved system. The current prototype includes some expediences that made it possible to create a working system in less than a year. The prototype FDL is one part of the overall project. There are other theoretical and experimental efforts that are described in other publications. The library described here contains definitions, theorems, theories, proof methods, and articles about topics in computational mathematics and books assembled from them. Currently it supports these objects created with the theorem proving systems MetaPRL, Nuprl and PVS. We intend to include material from other implemented logics such as Minlog, Coq, HOL, Isabelle, and Larch in due course. In addition to the purely formal material, the Library supports mathematically literate hypertext articles that cite and use the formal concepts. These include explanations of reference algorithms and explanations of formal mathematical models used in applications. Many operations on the Library are automated and extensible. The basic operations are to find and read material, organize it, and submit new material. New operations can be defined algorithmically. This manual is intended to help users understand the operation of the Library and to demonstrate to those interested in the project what else we intended to build and how it will be used