 How is interoperability between two systems to be enabled by CL? Suppose one of these systems is based on logic \(L\), and the other on \(L'\). (To ease exposition, assume that both logics are first-order.) The idea is that a theory \(\Phi_L\), that is, a set of formulae in \(L\), can be translated into CL, producing \(\Phi_{CL}\), and then this theory can be translated into \(\Phi_L'\). CL thus becomes an inter lingua. Note that what counts as a well-formed formula in \(L\) can be different than what counts as one in \(L'\). The two logics might also have different proof theories. For example, inference in \(L\) might be based on resolution, while inference in \(L'\) is of the natural deduction variety. Finally, the symbol sets will be different. Despite these differences, courtesy of the translations, desired behavior can be produced across the translation. That, at any rate, is the hope. The technical challenges here are immense, but federal monies are increasingly available for attacks on the problem of interoperability.