Skip to main content
PRL Project

Importing Mathematics from HOL into Nuprl

by Douglas J. Howe

In Theorem Proving in Higher Order Logics

  • unofficial copies PDF, PS

Nuprl and HOL are both tactic-based interactive theorem provers for higher-order logic, and both have been used in many substantial applications over the last decade. However, the HOL community has accumulated a much larger collection of formalized mathematics of the kind useful for hardware and software verification. This collection would be of great benefit in applying Nuprl to verification problems of real practical interest. This paper describes a connection we have implemented between HOL and Nuprl that gives Nuprl effective access to mathematics formalized in HOL. In designing this connection, we had to overcome a number of problems related to differences in the logics, logical infrastructures and stylistic conventions of Nuprl and HOL.

Supplementary material

bibTex ref: Howe96a

cite link