论文标题
通过转换为经典逻辑来解决量化的模态逻辑问题
Solving Quantified Modal Logic Problems by Translation to Classical Logics
论文作者
论文摘要
本文介绍了对自动定理证明（ATP）系统的评估（ATP）系统，该系统对从一阶模态逻辑问题的QMLTP库中提出的问题进行了评估。主要是，这些问题使用嵌入方式将TPTP语言中的一阶和高阶逻辑转换为键入的一阶和高阶逻辑，并使用一阶Resp解决。高阶逻辑ATP系统和模型发现器。此外，考虑了天然模态逻辑ATP系统的结果，并将其与嵌入方法的结果进行了比较。发现的结果是，嵌入过程是可靠且成功的，当将最新的ATP系统用作后端推理器时，一阶和高阶嵌入性能相似，本地模态逻辑ATP系统的性能与经典系统相当的性能，使用嵌入式嵌入的嵌入方式，通过嵌入本机的模态ATP的方法与嵌入式的方法相比，该方法与该方法相关的方法是不合时宜的。与本机模态系统相比，模态逻辑范围。
This article describes an evaluation of Automated Theorem Proving (ATP) systems on problems taken from the QMLTP library of first-order modal logic problems. Principally, the problems are translated to both typed first-order and higher-order logic in the TPTP language using an embedding approach, and solved using first-order resp. higher-order logic ATP systems and model finders. Additionally, the results from native modal logic ATP systems are considered, and compared with the results from the embedding approach. The findings are that the embedding process is reliable and successful when state-of-the-art ATP systems are used as backend reasoners, The first-order and higher-order embeddings perform similarly, native modal logic ATP systems have comparable performance to classical systems using the embedding for proving theorems, native modal logic ATP systems are outperformed by the embedding approach for disproving conjectures, and the embedding approach can cope with a wider range of modal logics than the native modal systems considered.
