Skip to main content


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:
Title: A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics.
Authors: Allen, Stuart F.
Bickford, Mark
Constable, Robert
Eaton, Richard
Kreitz, Christoph.
Keywords: computer science
technical report
Issue Date: 3-Feb-2003
Publisher: Cornell University
Abstract: 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 theories in a unified formal framework. The combined system is a first step towards a digital library of formalized mathematics that can be shared and used in complex applications.
Appears in Collections:Computing and Information Science Technical Reports

Files in This Item:

File Description SizeFormat
TR2003-1889.pdf189.65 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