Abstract
We have developed a proof translator from HOL into a classical extension of NuPRL which is based on two lines of previous work. First, it draws on earlier work by Doug Howe, who developed a translator of theorems from HOL into a classical extension of NuPRL which is justified by a hybrid set-theoretic/computational semantics. Second, we rely on our own previous work, which investigates this mapping from a proof-theoretic viewpoint and gives a constructive meta-logical proof of its soundness. In this paper the logical foundations of the embedding of HOL into this classical extension of NuPRL as well as technical aspects of the proof translator implementation are discussed.
| Original language | English (US) |
|---|---|
| Title of host publication | Theorem Proving in Higher Order Logics - 14th International Conference, TPHOLs 2001, Proceedings |
| Editors | Richard J. Boulton, Paul B. Jackson |
| Publisher | Springer-Verlag |
| Pages | 329-345 |
| Number of pages | 17 |
| ISBN (Print) | 354042525X, 9783540425250 |
| State | Published - Jan 1 2001 |
| Externally published | Yes |
| Event | 14th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2001 - Edinburgh, United Kingdom Duration: Sep 3 2001 → Sep 6 2001 |
Publication series
| Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
|---|---|
| Volume | 2152 |
| ISSN (Print) | 0302-9743 |
| ISSN (Electronic) | 1611-3349 |
Other
| Other | 14th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2001 |
|---|---|
| Country | United Kingdom |
| City | Edinburgh |
| Period | 9/3/01 → 9/6/01 |
ASJC Scopus subject areas
- Theoretical Computer Science
- Computer Science(all)
Fingerprint Dive into the research topics of 'The HOL/NuPRL proof translator a practical approach to formal interoperability'. Together they form a unique fingerprint.
Cite this
Naumov, P., Stehr, M. O., & Meseguer, J. (2001). The HOL/NuPRL proof translator a practical approach to formal interoperability. In R. J. Boulton, & P. B. Jackson (Eds.), Theorem Proving in Higher Order Logics - 14th International Conference, TPHOLs 2001, Proceedings (pp. 329-345). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2152). Springer-Verlag.