Solving Quantified Modal Logic Problems by Translation to Classical Logics

要約

この記事では、一次様相論理問題の QMLTP ライブラリから取得した問題に対する自動定理証明 (ATP) システムの評価について説明します。
主に、問題は埋め込みアプローチを使用して TPTP 言語の型付き 1 次ロジックと高次ロジックの両方に変換され、1 次それぞれの関数を使用して解決されます。
高次ロジック 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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google