論文の概要: Solving QMLTP Problems by Translation to Higher-order Logic
- arxiv url: http://arxiv.org/abs/2212.09570v1
- Date: Mon, 19 Dec 2022 16:02:14 GMT
- ステータス: 処理完了
- システム内更新日: 2022-12-20 18:26:54.846496
- Title: Solving QMLTP Problems by Translation to Higher-order Logic
- Title（参考訳）: 高階論理への変換によるQMLTP問題の解法
- Authors: Alexander Steen, Geoff Sutcliffe, Tobias Glei{\ss}ner, Christoph
Benzm\"uller
- Abstract要約: 本稿では,1次モーダル論理問題のQMライブラリから得られる問題に対して,ATP(Automated Theorem Proving)システムの評価を行う。
これらの問題は、埋め込み手法を用いてTPTP言語の高階論理に変換され、高階論理ATPシステムを用いて解決される。
- 参考スコア（独自算出の注目度）: 62.997667081978825
- License: http://creativecommons.org/licenses/by-nc-nd/4.0/
- Abstract: 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.
- Abstract（参考訳）: 本稿では,一階モーダル論理問題のqmltpライブラリから取り出された問題に対する自動定理証明(atp)システムの評価について述べる。
主に、この問題は埋め込み手法を用いてTPTP言語の高階論理に変換され、高階論理ATPシステムを用いて解決される。
さらに, ネイティブなモーダル論理ATPシステムの結果を, 組込み方式と比較して検討した。
結論は
i) 埋め込みプロセスは信頼性が高く成功している。
(II) バックエンドATPシステムの選択は, 組込み方式の性能に大きな影響を及ぼす可能性がある。
3) ネイティブなモーダル論理ATPシステムは埋め込みアプローチより優れている。
(4)埋め込み手法は、考慮されたネイティブなモーダルシステムよりも広い範囲のモーダル論理を扱うことができる。
関連論文リスト
- 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。