A Nuprl-PVS Connection:
Integrating Libraries of Formal Mathematics

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

Technical Report, Cornell University, Ithaca, NY, January 2003.


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.


BACK
Back to overview of papers


Bibtex Entry

@TechReport{tr:Allen+03a, author = "Stuart Allen and Mark Bickford and Robert Constable and Richard Eaton and Christoph Kreitz", title = "A {Nuprl-PVS} Connection: Integrating Libraries of Formal Mathematics", institution = "Cornell University. Department of Computer Science", year = "2003" }