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 languages 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 conclusions are that (i) The embedding process is reliable and successful. (ii) The choice of backend ATP system can significantly impact the performance of the embedding approach. (iii) Native modal logic ATP systems outperform the embedding approach. (iv) The embedding approach can cope with a wider range modal logics than the native modal systems considered.

本文对自动证明系统(Automated Theorem Proving, ATP)在一阶模态逻辑问题的QMLTP库中的表现进行了评估，主要采取了嵌入法将问题转换为TPTP语言中的高阶逻辑，使用高阶逻辑ATP系统进行求解，并将原生模态逻辑ATP系统的结果与嵌入法进行比较，得出结论：(一)嵌入过程是可靠和成功的；(二)后端ATP系统的选择会显著影响嵌入方法的性能；(三)原生模态逻辑ATP系统胜于嵌入方法；(四)嵌入方法可以处理比原生模态系统涵盖更广的模态逻辑。

将QMLTP问题翻译为高阶逻辑以求解