Importing Mathematics from HOL into Nuprl

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 veri cation. This collection would be of great bene t in applying Nuprl to veri cation problems of real practical interest. This paper describes a connection we have implemented between HOL and Nuprl that gives Nuprl e ective access to mathematics formalized in HOL. In designing this connection, we had to overcome a number of problems related to di erences in the logics, logical infrastructures and stylistic conventions of Nuprl and HOL.

• Type: Conference
• Year: 1996
• Where: TPHOL
• Authors: Douglas J. Howe
• Keywords: Automated Reasoning, HOL Community, Nuprl, TPHOL 1996, Veri Cation