JavaScript is disabled for your browser. Some features of this site may not work without it.
A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics.
| dc.contributor.author | Allen, Stuart F. | en_US |
| dc.contributor.author | Bickford, Mark | en_US |
| dc.contributor.author | Constable, Robert | en_US |
| dc.contributor.author | Eaton, Richard | en_US |
| dc.contributor.author | Kreitz, Christoph. | en_US |
| dc.date.accessioned | 2007-04-04T19:20:14Z | |
| dc.date.available | 2007-04-04T19:20:14Z | |
| dc.date.issued | 2003-02-03 | en_US |
| dc.identifier.citation | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2003-1889 | en_US |
| dc.identifier.uri | https://hdl.handle.net/1813/5605 | |
| dc.description.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. | en_US |
| dc.format.extent | 194204 bytes | |
| dc.format.mimetype | application/pdf | |
| dc.language.iso | en_US | en_US |
| dc.publisher | Cornell University | en_US |
| dc.subject | computer science | en_US |
| dc.subject | technical report | en_US |
| dc.title | A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics. | en_US |
| dc.type | technical report | en_US |
