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.
CITATION STYLE
Naumov, P., Stehr, M. O., & Meseguer, J. (2001). The HOL/NuPRL proof translator a practical approach to formal interoperability. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2152, pp. 329–345). Springer Verlag. https://doi.org/10.1007/3-540-44755-5_23
Mendeley helps you to discover research relevant for your work.