This paper 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 higher-order logic in the TPTP language using an embedding approach, and solved using higher-order logic ATP systems. Additionally, the results from native modal logic ATP systems are considered, and compared with those from the embedding approach. The findings are that the embedding process is reliable and successful, the choice of backend ATP system can significantly impact the performance of the embedding approach, native modal logic ATP systems outperform the embedding approach, and the embedding approach can cope with a wider range modal logics than the native modal systems considered.

翻译：本文评估了自动定理证明（ATP）系统在来自QMLTP一阶模态逻辑问题库上的表现。主要方法是将问题通过嵌入方式翻译成TPTP语言中的高阶逻辑，并使用高阶逻辑ATP系统求解。此外，本文还考虑了原生模态逻辑ATP系统的结果，并将其与嵌入方法的结果进行了比较。研究发现：嵌入过程可靠且成功，后端ATP系统的选择会显著影响嵌入方法的性能，原生模态逻辑ATP系统的表现优于嵌入方法，且嵌入方法能够处理比所考虑的原生模态系统更广泛的模态逻辑。