To illustrate the problems in relating logics as theories, we return to the problem of relating results in HOL to Nuprl. The HOL theory construction is similar to the Nuprl construction, except that HOL has a simpler classical type theory, and the construction has correspondingly fewer modules. The goal of relating HOL to Nuprl is shown by the dotted arrow between the HOL and Nuprl-HOL theories in Figure 3. Any such relation must justify the rules for each of the modules making up HOL from the rules in Nuprl.
Theory relations to justify one theory from another. In the 
example, the relation is stated so that results from HOL
can be used in Nuprl. The justification is in the opposite
direction: the HOL theory is justified in terms on the Nuprl theory,
providing a Nuprl interpretation of the HOL results.
Once this relation is made, the framework automatically translates the HOL results into Nuprl. This provides a raw interpretation of the HOL results, but it is also necessary to adapt the presentation because the existing Nuprl formalization of the rational numbers differs from the account in HOL. A common presentation must be chosen before the two theories can be combined. The first step in finding the relation is to provide a transformation between the basic representations used in the two theories. This provides a means for the logical environment to transform the remaining knowledge automatically, although intervention may be required to summarize the relation intuitively.
