Semantics-based filtering: Logic programming’s killer app?

Abstract

We present a logic programming based framework for rapidly translating one formal notation Ls to another formal notation Lt. The framework is based on Horn logical semantics—a logic programming encoding of formal semantics. A Horn logical semantics of the languageLs is constructed which employs the parse trees of the language Lt as semantic domains for expressing the meaning of sentences in Ls. 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.