Formal Logic Definitions for Interchange Languages
Formal Logic Definitions for Interchange Languages
复制标题
交换语言的形式逻辑定义
DOI：
--
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Florian Rabe
中科院分区：
文献类型：
--
作者：
Fulya Horozal;Florian Rabe
系统集成通常需要标准化的交换语言，通过这些语言系统可以交换数学知识。主要的例子是基于MathML的标记语言和TPTP。然而，这些语言只标准化了交换知识的语法，当涉及的逻辑复杂或众多时，这是不够的。另一方面，逻辑框架允许表示逻辑本身，因此知道语义，但它们从具体语法中抽象出来。
也许令人惊讶的是，直到最近，最先进的逻辑框架还不能充分表示形式系统中常用的逻辑。使用最近扩展的逻辑框架LF，我们展示了如何给出简洁的形式定义的逻辑中使用的TPTP。我们也可以正式定义各种TPTP逻辑之间的转换和组合。这允许我们构建语义感知工具支持，例如类型检查TPTP内容。
虽然我们的演讲集中在当前的TPTP逻辑，我们的方法可以很容易地扩展到其他逻辑和交换语言。特别是，我们的逻辑表示可以用于TPTP和MathML。因此，语义的单个定义可以与任一交换语法一起使用。
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.