論文の概要: Solving Quantified Modal Logic Problems by Translation to Classical Logics
- arxiv url: http://arxiv.org/abs/2212.09570v3
- Date: Mon, 29 Apr 2024 13:40:01 GMT
- ステータス: 処理完了
- システム内更新日: 2024-05-01 03:37:12.892401
- Title: Solving Quantified Modal Logic Problems by Translation to Classical Logics
- Title（参考訳）: 古典論理への翻訳による量子化モーダル論理問題の解法
- Authors: Alexander Steen, Geoff Sutcliffe, Christoph Benzmüller,
- Abstract要約: これらの問題は、埋め込みアプローチを用いて、型付き一階述語論理と高階述語論理の両方に変換される。
ネイティブなモーダル論理ATPシステムの結果について検討し, 組込み手法による結果と比較した。
- 参考スコア（独自算出の注目度）: 47.24825031148412
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: 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.
- Abstract（参考訳）: 本稿では,1次モーダル論理問題のQMLTPライブラリから得られる問題に対するATPシステムの評価について述べる。
主に、この問題はTPTP言語の型付き一階述語論理と高階述語論理の両方に埋め込みアプローチを用いて変換され、一階述語respを用いて解決される。
高階論理ATPシステムとモデルファインダ。
さらに, ネイティブなモーダル論理ATPシステムの結果も検討し, 組込み手法による結果と比較した。
その結果,1次および高次埋め込みは,古典的システムに匹敵する性能を有し,定理証明のための埋め込み,ネイティブなモーダル論理ATPシステムは,予想を証明するための埋め込みアプローチにより性能が向上し,組込みアプローチは考慮されたネイティブなモーダルシステムよりも広い範囲のモーダル論理に対処できることがわかった。
関連論文リスト
- Logic Agent: Enhancing Validity with Logic Rule Invocation [24.815341366820753]
Chain-of-Thoughtプロンプトは、推論タスク中に言語モデルの推論能力を増強するための重要なテクニックとして現れている。
本稿では,大規模言語モデルにおける推論プロセスの有効性向上を目的としたエージェントベースのフレームワークであるLogic Agent(LA)を紹介する。
論文 参考訳（メタデータ） (2024-04-28T10:02:28Z) - LINC: A Neurosymbolic Approach for Logical Reasoning by Combining
Language Models with First-Order Logic Provers [60.009969929857704]
論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。
本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。
我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
論文 参考訳（メタデータ） (2023-10-23T17:58:40Z) - Modeling Hierarchical Reasoning Chains by Linking Discourse Units and
Key Phrases for Reading Comprehension [80.99865844249106]
本稿では,論理的推論の基盤として,対話レベルと単語レベルの両方の文脈を扱う総合グラフネットワーク(HGN)を提案する。
具体的には、ノードレベルの関係とタイプレベルの関係は、推論過程におけるブリッジと解釈できるが、階層的な相互作用機構によってモデル化される。
論文 参考訳（メタデータ） (2023-06-21T07:34:27Z) - An optimized fuzzy logic model for proactive maintenance [0.0]
ITTFLMは5msで出力を生成でき、このモデルでは、トラペゾイダルのメンバーシップ関数に基づくモデルが高精度に故障状態を識別することを示した。
ITTFLMは、植物機械からリアルタイムで収集されたファンデータに基づいてテストされた。
論文 参考訳（メタデータ） (2022-12-24T15:49:46Z) - Discourse-Aware Graph Networks for Textual Logical Reasoning [142.0097357999134]
パッセージレベルの論理関係は命題単位間の係り合いまたは矛盾を表す(例、結論文)
論理的推論QAを解くための論理構造制約モデリングを提案し、談話対応グラフネットワーク(DAGN)を導入する。
ネットワークはまず、インラインの談話接続とジェネリック論理理論を利用した論理グラフを構築し、その後、エッジ推論機構を用いて論理関係を進化させ、グラフ機能を更新することで論理表現を学習する。
論文 参考訳（メタデータ） (2022-07-04T14:38:49Z) - Linear Temporal Logic Modulo Theories over Finite Traces (Extended
Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。
命題の文字は任意の理論で解釈された一階述語式に置き換えられる。
Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文 参考訳（メタデータ） (2022-04-28T17:57:33Z) - Neuro-Symbolic Inductive Logic Programming with Logical Neural Networks [65.23508422635862]
我々は最近提案された論理ニューラルネットワーク(LNN)を用いた学習規則を提案する。
他のものと比較して、LNNは古典的なブール論理と強く結びついている。
標準ベンチマークタスクの実験では、LNNルールが極めて解釈可能であることを確認した。
論文 参考訳（メタデータ） (2021-12-06T19:38:30Z) - ORCHARD: A Benchmark For Measuring Systematic Generalization of
Multi-Hierarchical Reasoning [8.004425059996963]
本稿では,Transformer と LSTM のモデルが体系的一般化において驚くほど失敗することを示す。
また、階層間の参照の増加に伴い、Transformerはランダムにしか動作しないことを示す。
論文 参考訳（メタデータ） (2021-11-28T03:11:37Z) - Refining Labelled Systems for Modal and Constructive Logics with
Applications [0.0]
この論文は、モーダル論理や構成論理のセマンティクスを「経済的な」証明システムに変換する手段として機能する。
精製法は、ラベル付きおよびネストされたシーケント計算の2つの証明理論パラダイムを結合する。
導入された洗練されたラベル付き電卓は、デオン性STIT論理に対する最初の証明探索アルゴリズムを提供するために使用される。
論文 参考訳（メタデータ） (2021-07-30T08:27:15Z) - Public Announcement Logic in HOL [0.0]
関連する共通知識を持つ公開告知論理のための浅層セマンティック埋め込みについて述べる。
この埋め込みにより、古典的な高階論理に対するオフ・ザ・シェルフ定理証明を用いて、この論理を初めて自動化することができる。
論文 参考訳（メタデータ） (2020-10-02T06:46:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。