Now showing items 1-3 of 3

    • FDL: A Prototype Formal Digital Library 

      Allen, Stuart; Bickford, Mark; Constable, Robert; Eaton, Richard; Kreitz, Christoph; Lorigo, Lor (Cornell University, 2004-06-16)
      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 ...
    • A Graph-Based Approach towards Discerning Inherent Structures in a Digital Library of Formal Mathematics 

      Lorigo, Lori; Kleinberg, Jon; Eaton, Richard; Constable, Robert (Cornell University, 2006-01-30)
      As the amount of online formal mathematical content grows, for example through active efforts such as the Mathweb [21], MOWGLI [4], Formal Digital Library, or FDL [1], and others, it becomes increasingly valuable to find ...
    • A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics. 

      Allen, Stuart F.; Bickford, Mark; Constable, Robert; Eaton, Richard; Kreitz, Christoph. (Cornell University, 2003-02-03)
      We describe a link between the Nuprl and PVS proof systems that enables users to access PVS from the Nuprl theorem proving environment, to import PVS theories into the Nuprl library, and to browse both Nuprl and PVS ...