Formal Interoperbility in Theorem Proving

Keywords: General Logics, Formal Interoperabilty, Theorem Prover, HOL, Nuprl, Maude, Meta-Tool, HOL-Nuprl Connection, Logic Translator

In this project we investigate the use of general logics introduced by Meseguer 1989 in the context of formal interoperabilty between theorem provers. As a typical and practically relevant example we study the HOL-Nuprl Connection proposed by Doug Howe from a proof-theoretic perspective.

The HOL theorem proving system has a rich library of theories that can save a lot of effort by not having to specify from scratch many commonly encountered theories. Potentially, this is a very useful resource not only for HOL, but for other theorem proving systems based on other logics. Howe defined a map of logics mapping the HOL logic into the logic of Nuprl, and implemented such a mapping to make possible the translation from HOL theories to Nuprl theories. In this way, the practical goal of relating both systems and making the HOL libraries available to Nuprl was achieved. However, the translation itself was carried out by conventional means, and therefore was not in a form suitable for metalogical analysis.

After studying this mapping with the kind help of Doug Howe, Robert Constable and Stuart Allen, we have recently formally specified it in Maude. The result is an executable formal specification of the mapping that translates HOL theories into Nuprl theories. Large HOL libraries have already been translated into Nuprl this way.

In order to verify the correctness of the translation, we have investigated, in parallel with the work summarized above, an abstract version of the mapping in the categorical framework of general logics. In [3] we have proved a strong correctness result, namely, that the mapping is actually a mapping between the entailment systems of HOL and a classical variant of Nuprl. This result is of a proof-theoretic nature and hence complementary to the semantical argument given by Howe. Beyond its role as a direct justification for the translator, this result suggests an interesting new direction, namely, extending the mapping between entailment systems to a mapping between proof calculi, which would mean in practice that theorems could be translated together with their proofs. Recent progress on the development of such a proof translator on the top of the Nuprl system is reported in the reference [4] below.

Relevant References:

1. Manuel Clavel, Francisco Duran, Steven Eker, Jose Meseguer, Mark-Oliver Stehr: Maude as a Formal Meta-Tool. In the proceedings of FM'99, The World Congress On Formal Methods. Toulouse, France, September 20-24, 1999. Also appeared in the book OBJ/CafeOBJ/Maude at Formal Methods '99, Kokichi Futatsugi, Joseph Goguen and Jose Meseguer (Eds.), Theta (Bucharest), September 1999, ISBN 973-99097-1-X.
2. Mark-Oliver Stehr: Justifying the HOL-Nuprl Connection in the Categorical Framework of General Logics (Talk given at Cornell)
3. Mark-Oliver Stehr, Pavel Naumov, Jose Meseguer: A Proof-Theoretic Approach to the HOL-Nuprl Connection with Applications to Proof-Translation (extended abstract), In WADT/CoFI'01, 15th International Workshop on Algebraic Development Techniques and General Workshop of the CoFI WG, Genova, Italy, April 1 - 3, 2001, Proceedings. Full version available here.
4. Pavel Naumov, Mark-Oliver Stehr, Jose Meseguer: The HOL/NuPRL Proof Translator - A Practical Approach to Formal Interoperability , Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs'2001, Edinburgh, Scottland, UK , September 3 - 6, 2001, Proceedings, volume 2152 of Lecture Notes in Computer Science, © Springer-Verlag , 2001.