TSTP Data-Exchange Formats for Automated Theorem Proving Tools
TSTP Data-Exchange Formats for Automated Theorem Proving Tools
复制标题
自动定理证明工具的 TSTP 数据交换格式
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
S. Schulz
中科院分区：
文献类型：
--
作者：
G. Sutcliffe;J. Zimmer;S. Schulz
本文介绍了两种数据交换格式的自动定理证明（ATP）工具。首先，描述了用于编写输入到ATP系统的问题和用于编写从ATP系统输出的解决方案的语言。其次，描述了用于指定ATP问题的逻辑状态的值的层次结构，如可以由ATP系统建立的。这些数据交换格式将支持ATP的应用和研究，并将促进分布式和嵌入式环境中ATP工具之间的通信。
This paper describes two data-exchange formats for Automated Theorem Proving (ATP) tools. First, a language for writing the problems that are input to ATP systems, and for writing the solutions that are output from ATP systems, is described. Second, a hierarchy of values for specifying the logical status of an ATP problem, as may be established by an ATP system, is described. These data-exchange formats will support application and research in ATP, and will facilitate communication between ATP tools in distributed and embedded environments.