However, an interlingua with the expressive power of first-order logic, such as the Knowledge Interchange Format (KIF) being developed in the ARPA Knowledge Sharing Effort [Genesereth & Fikes 92], can provide that support for a broad spectrum of theories and languages. For our purposes in this paper, we will assume an interlingua and a set of languages for which the properties listed above hold.

The interlingua-based translation process can be thought of as consisting of three major steps:

? Translation from the source language into a subset of the interlingua;

? Translation between subsets of the interlingua; and

? Translation from a subset of the interlingua into the target language.

Since the interlingua is assumed to be at least as expressive as the source language, the first translation step into the interlingua can typically be specified in the form of a grammar that describes how each top-level form (e.g., sentence, definition, rule) in the source language translates into the interlingua. In this paper we specify the conditions under which such a grammar is reversible so that the grammar can also be used to translate out of the interlingua. If one has such a reversible grammar for the target language, then step 2 involves translating from the subset of the interlingua produced by the source language grammar to the subset of the interlingua that is translated (i.e., recognized) by the reverse of the target language grammar. For any given top-level form Fs in the source subset, translation step 2 involves determining a top-level form Ft in the target subset such that Fs is logically equivalent to Ft. Thus, formally, step 2 requires hypothesizing an equivalent form in the target subset and then proving the equivalence.

Step 2 of the translation process is the difficult one for most languages. However, steps 1 and 3 are far from trivial. In this paper, we present formal languages and methods that are adequate for doing steps 1 and 3. In particular, we:

? Formally describe the translation process into and out of an interlingua;

? Present a method for determining whether a given grammar in fact specifies how to construct a translation for every top level form in a given source language; and

? Present a method for determining whether a given grammar is reversible so that it can be used to translate both into and out of an interlingua.

These languages and methods have been incorporated into a "translator shell" system that provides facilities for specifying interlingua-based translation using KIF as the interlingua. The system has been used to build translators for multiple representation languages and those translators have successfully translated non-trivial knowledge bases. The examples in this paper are taken from two of these grammars: a CLASSIC [Borgida, et al 89] to KIF grammar and a LOOM [MacGregor 91] to KIF grammar. The CLASSIC to KIF grammar is used in a bi-directional translator [Fikes, et al 91], and the LOOM to KIF grammar is used in a bi-directional translator currently under development.

2. Interlingua-Based Translations and Semantics

We consider here equivalence preserving translations [Buvac and Fikes 93] in which the translation of an axiomatization of a logical theory is an axiomatization of an equivalent logical theory. To make such a requirement on translators meaningful, a declarative semantics including logical entailment needs to be formally specified for both the source and target languages. We are assuming such a declarative semantics for the interlingua.