Skip to main content


eCommons@Cornell

eCommons@Cornell >
Faculty of Computing and Information Science >
Computing and Information Science >
Computing and Information Science Technical Reports >

Please use this identifier to cite or link to this item: http://hdl.handle.net/1813/5652
Title: FDL: A Prototype Formal Digital Library
Authors: Allen, Stuart
Bickford, Mark
Constable, Robert
Eaton, Richard
Kreitz, Christoph
Lorigo, Lor
Keywords: computer science
technical report
Issue Date: 16-Jun-2004
Publisher: Cornell University
Citation: http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2004-1941
Abstract: 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.
URI: http://hdl.handle.net/1813/5652
Appears in Collections:Computing and Information Science Technical Reports

Files in This Item:

File Description SizeFormat
TR2004-1941.pdf459.14 kBAdobe PDFView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.

 

© 2014 Cornell University Library Contact Us