We present a logic programming based framework for rapidly translating one formal notation to another formal notation . The framework is based on Horn logical semantics—a logic programming encoding of formal semantics. A Horn logical semantics of the language is constructed which employs the parse trees of the language as semantic domains for expressing the meaning of sentences in . This formal semantics, coded in logic programming, immediately yields an executable (reversible) filter. This (reversible) filter is provably correct, as it is generated from the semantic specification. Our approach provides a formal basis for interoperability and is illustrated through five major practical applications: Translating Nemeth Math Braille notation to LaTEX, translating HTML to VoiceXML to make web-pages accessible via an audio-browser or a phone, translating ODBC programs/data to OQL (Object Query Language) programs/data, automatically generating validating parsers for XML, and interoperating between various biological software systems developed for phylogenetic inference via the NEXUS data representation language.