Formal logic definitions for interchange languages

Abstract

System integration often requires standardized interchange languages, via which systems can exchange mathematical knowledge. Major examples are the MathML-based markup languages and TPTP. However, these languages standardize only the syntax of the exchanged knowledge, which is insufficient when the involved logics are complex or numerous. Logical frameworks, on the other hand, allow representing the logics themselves (and are thus aware of the semantics), but they abstract from the concrete syntax. Maybe surprisingly, until recently, state-of-the-art logical frameworks were not quite able to adequately represent logics commonly used in formal systems. Using a recent extension of the logical framework LF, we show how to give concise formal definitions of the logics used in TPTP. We can also formally define translations and combinations between the various TPTP logics. This allows us to build semantics-aware tool support such as type-checking TPTP content. While our presentation focuses on the current TPTP logics, our approach can be easily extended to other logics and interchange languages. In particular, our logic representations can be used with both TPTP and MathML. Thus, a single definition of the semantics can be used with either interchange syntax.