論文の概要: Automating Reasoning with Standpoint Logic via Nested Sequents
- arxiv url: http://arxiv.org/abs/2205.02749v1
- Date: Thu, 5 May 2022 16:27:57 GMT
- ステータス: 処理完了
- システム内更新日: 2022-05-06 17:19:54.541954
- Title: Automating Reasoning with Standpoint Logic via Nested Sequents
- Title（参考訳）: Nested Sequentsによるスタンドポイント論理による推論の自動化
- Authors: Tim S. Lyon and Luc\'ia G\'omez \'Alvarez
- Abstract要約: スタンドポイント論理は多面的アプローチを提唱し、多種多様で恐らく矛盾するスタンドポイントの選択による推論を許容する。
非決定論的証明探索アルゴリズムを用いて視点推論を自動化する方法を示す。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Standpoint logic is a recently proposed formalism in the context of knowledge
integration, which advocates a multi-perspective approach permitting reasoning
with a selection of diverse and possibly conflicting standpoints rather than
forcing their unification. In this paper, we introduce nested sequent calculi
for propositional standpoint logics--proof systems that manipulate trees whose
nodes are multisets of formulae--and show how to automate standpoint reasoning
by means of non-deterministic proof-search algorithms. To obtain worst-case
complexity-optimal proof-search, we introduce a novel technique in the context
of nested sequents, referred to as "coloring," which consists of taking a
formula as input, guessing a certain coloring of its subformulae, and then
running proof-search in a nested sequent calculus on the colored input. Our
technique lets us decide the validity of standpoint formulae in CoNP since
proof-search only produces a partial proof relative to each permitted coloring
of the input. We show how all partial proofs can be fused together to construct
a complete proof when the input is valid, and how certain partial proofs can be
transformed into a counter-model when the input is invalid. These
"certificates" (i.e. proofs and counter-models) serve as explanations of the
(in)validity of the input.
- Abstract（参考訳）: 立場論理は知識統合の文脈で最近提案された形式主義であり、多面的アプローチを提唱し、統一を強制するのではなく、多様でおそらく矛盾する立場から推論を許す。
本稿では,ノードが複数集合の論理式を持つ木を操り,非決定論的証明探索アルゴリズムを用いて視点推論を自動化する方法を示す。
入力として公式を取り、そのサブフォルムの特定の色を推測し、その色入力でネストしたシークエント計算で証明探索を行う「色付け」と呼ばれる、ネスト化されたシークエントの文脈において、最悪の場合の最適証明探索を行う新しい手法を導入する。
提案手法は,各入力の許容色に対する部分的証明のみを生成するため,CoNPにおけるスタンドポイント式の有効性を判定する。
入力が有効であれば,すべての部分的証明を融合して完全な証明を構築する方法と,入力が無効な場合には,ある部分的証明をカウンターモデルに変換する方法を示す。
これらの「証明(certificates)」(すなわち証明と反モデル)は、入力の(in)validityの説明として役立ちます。
関連論文リスト
- $O_2$ is a multiple context-free grammar: an implementation-, formalisation-friendly proof [0.0]
それらを生成することができる文法の表現力に応じて言語を分類することは、計算言語学における根本的な問題である。
本稿では,各証明が検証された(すなわち,証明支援者によってチェックされる)アルゴリズムに繋がるかどうかを,MCFGを通して解析できるかどうかを体系的に研究する,計算的および証明理論的な視点から,既存の証明を解析する。
論文 参考訳（メタデータ） (2024-05-15T14:51:11Z) - MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳（メタデータ） (2024-02-14T05:57:58Z) - Automated Completion of Statements and Proofs in Synthetic Geometry: an
Approach based on Constraint Solving [0.0]
不完全予想と不完全証明を完遂する枠組みを提案する。
このフレームワークは、不足した仮定を持つ予想を適切な定理に変えることができる。
また、提案したフレームワークは、人間の読みやすいマシンチェック可能な証明に証明スケッチを完成させるのに役立ちます。
論文 参考訳（メタデータ） (2024-01-22T12:49:08Z) - Verifying Quantum Phase Estimation (QPE) using Prove-It [0.0]
Prove-Itと呼ばれる汎用的な対話型定理証明アシスタントは、量子位相推定(QPE)アルゴリズムを検証するために使用された。
Prove-Itは、量子回路に関するステートメントを含む洗練された数学的ステートメントを表現する能力に特有である。
論文 参考訳（メタデータ） (2023-04-05T01:21:00Z) - Logical Satisfiability of Counterfactuals for Faithful Explanations in
NLI [60.142926537264714]
本稿では, 忠実度スルー・カウンタファクトの方法論について紹介する。
これは、説明に表される論理述語に基づいて、反実仮説を生成する。
そして、そのモデルが表現された論理と反ファクトの予測が一致しているかどうかを評価する。
論文 参考訳（メタデータ） (2022-05-25T03:40:59Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。
NLProofSは仮説に基づいて関連するステップを生成することを学習する。
EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文 参考訳（メタデータ） (2022-05-25T02:22:30Z) - Logical Credal Networks [87.25387518070411]
本稿では,論理と確率を組み合わせた先行モデルの多くを一般化した表現的確率論的論理である論理的クレダルネットワークを紹介する。
本稿では,不確実性のあるマスターミンドゲームを解くこと,クレジットカード詐欺を検出することを含む,最大後部推論タスクの性能について検討する。
論文 参考訳（メタデータ） (2021-09-25T00:00:47Z) - multiPRover: Generating Multiple Proofs for Improved Interpretability in
Rule Reasoning [73.09791959325204]
我々は、自然言語の事実と規則の形で明示的な知識を推論することを目的としている言語形式推論の一種に焦点を当てる。
PRoverという名前の最近の研究は、質問に答え、答えを説明する証明グラフを生成することによって、そのような推論を行う。
本研究では,自然言語規則ベースの推論のために複数の証明グラフを生成するという,新たな課題に対処する。
論文 参考訳（メタデータ） (2021-06-02T17:58:35Z) - Prove-It: A Proof Assistant for Organizing and Verifying General
Mathematical Knowledge [0.0]
Prove-ItはPythonベースの汎用的対話型定理証明アシスタントである。
Prove-ItはフレキシブルなJupyterノートブックベースのユーザーインターフェイスを使って、対話や証明の手順を文書化している。
現在の開発と今後の研究には、量子回路操作と量子アルゴリズム検証への有望な応用が含まれている。
論文 参考訳（メタデータ） (2020-12-20T18:15:12Z) - Foundations of Reasoning with Uncertainty via Real-valued Logics [70.43924776071616]
我々は、本質的にすべての実数値論理をカバーするためにパラメータ化できる、音と強完全公理化を与える。
文のクラスは非常に豊かであり、各クラスは実数値論理の式の集合に対して可能な実値の集合を記述する。
論文 参考訳（メタデータ） (2020-08-06T02:13:11Z) - Understanding the QuickXPlain Algorithm: Simple Explanation and Formal
Proof [0.0]
本稿では,Ulrich Junker の QuickXPlain アルゴリズムの正当性を示す。
他のアルゴリズムを証明するためのガイダンスとして使用できる。
また、QuickXPlainによって計算された結果に依存するシステムの"ギャップレス"な正しさを提供する可能性も提供する。
論文 参考訳（メタデータ） (2020-01-07T01:37:41Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。