Solving QMLTP Problems by Translation to Higher-order Logic

要約

この論文では、一次様相論理問題の QMLTP ライブラリから取得した問題に対する自動定理証明 (ATP) システムの評価について説明します。
主に、問題は埋め込みアプローチを使用して TPTP 言語の高次ロジックに変換され、高次ロジック ATP システムを使用して解決されます。
さらに、ネイティブ モーダル ロジック ATP システムからの結果が考慮され、埋め込みアプローチからの結果と比較されます。
その結果、埋め込みプロセスは信頼性が高く成功していること、バックエンド ATP システムの選択は埋め込みアプローチのパフォーマンスに大きな影響を与える可能性があること、ネイティブ モーダル ロジック ATP システムは埋め込みアプローチよりも優れたパフォーマンスを示し、埋め込みアプローチはより広範囲のモーダル ロジックに対応できることが判明しました。
考慮されているネイティブモーダルシステムよりも。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google