論文の概要: Modal Logic S5 Satisfiability in Answer Set Programming

• arxiv url: http://arxiv.org/abs/2108.04194v1
• Date: Mon, 9 Aug 2021 17:35:31 GMT
• ステータス: 処理完了
• システム内更新日: 2021-08-10 15:34:46.228177
• Title: Modal Logic S5 Satisfiability in Answer Set Programming
• Title（参考訳）: 解集合プログラミングにおけるモーダル論理S5の満足度
• Authors: Mario Alviano, Sotiris Batsakis, George Baryannis
• Abstract要約: 我々は、あらゆる世界に関係のある命題的原子の実装にAnswer Set Programmingを使うことを提案する。 提案したエンコーディングは、モーダル演算子によって根付いた部分形式間の包含関係などの他の特性を利用するように設計されている。 提案したエンコーディングの実証評価により, 到達性関係は非常に効果的であり, 最先端のS5ソルバに匹敵する性能を示した。
• 参考スコア（独自算出の注目度）: 8.89493507314525
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Modal logic S5 has attracted significant attention and has led to several practical applications, owing to its simplified approach to dealing with nesting modal operators. Efficient implementations for evaluating satisfiability of S5 formulas commonly rely on Skolemisation to convert them into propositional logic formulas, essentially by introducing copies of propositional atoms for each set of interpretations (possible worlds). This approach is simple, but often results into large formulas that are too difficult to process, and therefore more parsimonious constructions are required. In this work, we propose to use Answer Set Programming for implementing such constructions, and in particular for identifying the propositional atoms that are relevant in every world by means of a reachability relation. The proposed encodings are designed to take advantage of other properties such as entailment relations of subformulas rooted by modal operators. An empirical assessment of the proposed encodings shows that the reachability relation is very effective and leads to comparable performance to a state-of-the-art S5 solver based on SAT, while entailment relations are possibly too expensive to reason about and may result in overhead. This paper is under consideration for acceptance in TPLP.
• Abstract（参考訳）: モーダル論理 S5 は、ネストしたモーダル演算子を扱うための単純化されたアプローチのため、いくつかの実用的応用につながっている。 s5の公式の満足性を評価するための効率的な実装は、一般的にはスコーレム化に依存して命題論理式に変換し、基本的には各解釈集合(可能世界)に対して命題原子のコピーを導入する。 このアプローチは単純であるが、しばしば処理が難しい大きな公式になってしまうため、より控えめな構成が必要となる。 本研究では,このような構成の実装にAnswer Set Programmingを用いること,特に,到達可能性関係を用いて,すべての世界に関係する命題原子を特定することを提案する。 提案する符号化は、モーダル作用素が根ざした部分形式関係などの他の性質を利用するように設計されている。 提案する符号化の実験的評価は,到達可能性の関係が非常に効果的であり,satに基づく最先端のs5ソルバに匹敵する性能を示す。 本論文はTPLPの受容について検討中である。

関連論文リスト

• Think Beyond Size: Adaptive Prompting for More Effective Reasoning [0.0]
  本稿では,動的かつ反復的なフレームワークであるAdaptive Promptingを紹介する。 その結果、Adaptive Promptingは、算術的推論(GSM8K、MultiArithm)、論理的推論、コモンセンスタスクなど、様々な推論ベンチマークのパフォーマンスを著しく向上させることを示した。 提案手法は,計算効率を維持しつつ,GPT-4などの大規模モデルと競合する性能を実現する。
  論文  参考訳（メタデータ） (2024-10-10T17:14:36Z)
• The Foundations of Tokenization: Statistical and Computational Concerns [51.370165245628975]
  トークン化は、NLPパイプラインにおける重要なステップである。 NLPにおける標準表現法としての重要性は認識されているが、トークン化の理論的基盤はまだ完全には理解されていない。 本稿では,トークン化モデルの表現と解析のための統一的な形式的枠組みを提案することによって,この理論的ギャップに対処することに貢献している。
  論文  参考訳（メタデータ） (2024-07-16T11:12:28Z)
• Large Language Models as an Indirect Reasoner: Contrapositive and Contradiction for Automated Reasoning [74.90592233107712]
  本稿では,直接推論 (DR) と間接推論 (IR) を並列な複数の推論経路として考慮し,最終解を導出する直接間接推論 (DIR) 手法を提案する。 我々のDIR法は単純だが有効であり、既存のCoT法と簡単に統合できる。
  論文  参考訳（メタデータ） (2024-02-06T03:41:12Z)
• ExeDec: Execution Decomposition for Compositional Generalization in Neural Program Synthesis [54.18659323181771]
  プログラム合成において望ましいいくつかの異なる構成一般化形式を特徴付ける。 本稿では,ExeDecを提案する。ExeDecは,実行サブゴールを予測し,各ステップでプログラム実行によって段階的に通知される問題を解くための,新しい分解ベースの戦略である。
  論文  参考訳（メタデータ） (2023-07-26T01:07:52Z)
• From Robustness to Explainability and Back Again [3.7950144463212134]
  本稿では、形式的説明可能性のスケーラビリティの低さに対処し、形式的説明を計算するための新しい効率的なアルゴリズムを提案する。 提案アルゴリズムは、代わりに複数のクエリに答えることによって説明を計算し、そのようなクエリの数は、機能数に対して最も線形であるように頑健である。
  論文  参考訳（メタデータ） (2023-06-05T17:21:05Z)
• Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving [0.3441021278275805]
  確率的プログラミングは、一般的なコンピュータプログラミング、統計的推論、形式的意味論を組み合わせたものである。 ProbURelは、Hehnerの予測確率的プログラミングに基づいているが、彼の作品が広く採用されるにはいくつかの障害がある。 コントリビューションには、Unified Theories of Programming(UTP)を使用した関係の形式化や、ブラケット外の確率などが含まれています。 ロボットのローカライゼーションの問題,機械学習の分類,確率ループの終了など,6つの事例で研究成果を実演する。
  論文  参考訳（メタデータ） (2023-03-16T23:36:57Z)
• Semantic-aware Modular Capsule Routing for Visual Question Answering [55.03883681191765]
  SuPER と呼ばれるセマンティック・アウェアな modUlar caPsulE フレームワークを提案する。 5つのベンチマークデータセットに対して提案した SUPER スキームの有効性と一般化能力を比較検討した。
  論文  参考訳（メタデータ） (2022-07-21T10:48:37Z)
• Rationale-Augmented Ensembles in Language Models [53.45015291520658]
  我々は、数発のテキスト内学習のための合理化促進策を再考する。 我々は、出力空間における合理的サンプリングを、性能を確実に向上させるキーコンポーネントとして特定する。 有理拡張アンサンブルは既存のプロンプト手法よりも正確で解釈可能な結果が得られることを示す。
  論文  参考訳（メタデータ） (2022-07-02T06:20:57Z)
• Linear Temporal Logic Modulo Theories over Finite Traces (Extended Version) [72.38188258853155]
  有限トレース(LTLf)上の線形時間論理について検討する。 命題の文字は任意の理論で解釈された一階述語式に置き換えられる。 Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
  論文  参考訳（メタデータ） (2022-04-28T17:57:33Z)
• Adaptive n-ary Activation Functions for Probabilistic Boolean Logic [2.294014185517203]
  マッチングやアリティ向上の活性化関数を用いて,任意の論理を単一層で学習できることが示される。 我々は,非ゼロパラメータの数を信念関数の有効アリティに直接関連付ける基礎を用いて,信念表を表現する。 これにより、パラメータの間隔を誘導することで論理的複雑性を低減する最適化アプローチが開かれる。
  論文  参考訳（メタデータ） (2022-03-16T22:47:53Z)
• String Theories involving Regular Membership Predicates: From Practice to Theory and Back [12.98284167710378]
  文字列制約系に対する満足度問題に対するアルゴリズムは、対象ケースに存在する制約の構造を徹底的に理解する必要がある。 本稿では,正規表現構成述語を含む文献で提示されるベンチマークを調査し,異なる一階述語論理理論を抽出し,決定不能性を証明する。 特に、現実世界のベンチマークで最も一般的な理論はPSPACE完全であり、文字列制約を解決するためのより効率的なアルゴリズムの実装に直結する。
  論文  参考訳（メタデータ） (2021-05-15T13:13:50Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。