A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics.

Allen, Stuart F.; Bickford, Mark; Constable, Robert; Eaton, Richard; Kreitz, Christoph.

A Nuprl-PVS Connection: Integrating Libraries of Formal Mathematics.

File(s)

TR2003-1889.pdf (189.65 KB)

Permanent Link(s)

https://hdl.handle.net/1813/5605

Collections

Computing and Information Science Technical Reports

Author

Allen, Stuart F.

Bickford, Mark

Constable, Robert

Eaton, Richard

Kreitz, Christoph.

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.

Date Issued

2003-02-03

Publisher

Cornell University

Keywords

computer science

•

technical report

Previously Published as

http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cis/TR2003-1889

Type

technical report