System Description : JGXYZ An ATP System for Gap and Glut Logics
System Description : JGXYZ An ATP System for Gap and Glut Logics
复制标题
系统描述：JGXYZ 用于缺口和过剩逻辑的 ATP 系统
DOI：
10.1007/978-3-030-29436-6_31
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Pelletier, F.J.
中科院分区：
文献类型：
--
作者：
Sutcliffe, G.;Pelletier, F.J.
本文描述了一个名为 JGXYZ 的 ATP 系统，用于某些缺口和过剩逻辑。 JGXYZ 基于对 FOL 的等价可证明翻译，然后使用现有的 FOL ATP 系统。 JGXYZ 的一个关键特征是到 FOL 的转换是数据驱动的，从某种意义上说，它只需要为一元和二元连接词添加新逻辑的真值表，以便为该逻辑生成 ATP 系统。 JGXYZ 的实验结果说明了逻辑和翻译问题之间的差异，无论是在技术上还是在准现实世界用例方面。
This paper describes an ATP system, named JGXYZ, for some gap and glut logics. JGXYZ is based on an equi-provable translation to FOL, followed by use of an existing ATP system for FOL. A key feature of JGXYZ is that the translation to FOL is data-driven, in the sense that it requires only the addition of a new logic’s truth tables for the unary and binary connectives in order to produce an ATP system for the logic. Experimental results from JGXYZ illustrate the differences between the logics and translated problems, both technically and in terms of a quasi-real-world use case.