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.

翻译：本文针对一阶模态逻辑问题库QMLTP中的问题，对自动定理证明（ATP）系统进行了评估研究。主要采用嵌入方法，将问题转化为TPTP语言中的有类型一阶逻辑和高阶逻辑，并使用一阶逻辑与高阶逻辑的ATP系统及模型查找器进行求解。此外，本文还考察了原生模态逻辑ATP系统的求解结果，并将其与嵌入方法的结果进行了比较。研究发现：当使用最先进的ATP系统作为后端推理器时，嵌入过程可靠且成功；一阶逻辑与高阶逻辑的嵌入方法表现相似；在定理证明方面，原生模态逻辑ATP系统的性能与采用嵌入方法的经典系统相当；在猜想反例构造方面，原生模态逻辑ATP系统的表现不及嵌入方法；此外，嵌入方法能够处理的模态逻辑范围比所考虑的原生模态系统更为广泛。