|
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/5605
| 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 |
| Citation: | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2003-1889 |
| 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. |
| URI: | http://hdl.handle.net/1813/5605 |
| Appears in Collections: | Computing and Information Science Technical Reports
|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.
|
