論文の概要: Contradictions
- arxiv url: http://arxiv.org/abs/2509.07026v1
- Date: Sun, 07 Sep 2025 13:47:51 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-09-10 14:38:27.036525
- Title: Contradictions
- Title(参考訳): 矛盾
- Authors: Yang Xu, Shuwei Chen, Xiaomei Zhong, Jun Liu, Xingxing He,
- Abstract要約: 本稿では,標準矛盾を体系的に構築することに焦点を当てる。
本稿では,最大標準矛盾による節集合の満足度と不満足度を決定する手法を提案する。
最大三角形標準矛盾と三角型標準矛盾の両方に埋め込まれた標準部分矛盾の数を計算するための公式を導出する。
- 参考スコア(独自算出の注目度): 9.602468627573215
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Trustworthy AI requires reasoning systems that are not only powerful but also transparent and reliable. Automated Theorem Proving (ATP) is central to formal reasoning, yet classical binary resolution remains limited, as each step involves only two clauses and eliminates at most two literals. To overcome this bottleneck, the concept of standard contradiction and the theory of contradiction-separation-based deduction were introduced in 2018. This paper advances that framework by focusing on the systematic construction of standard contradictions. Specially, this study investigates construction methods for two principal forms of standard contradiction: the maximum triangular standard contradiction and the triangular-type standard contradiction. Building on these structures, we propose a procedure for determining the satisfiability and unsatisfiability of clause sets via maximum standard contradiction. Furthermore, we derive formulas for computing the number of standard sub-contradictions embedded within both the maximum triangular standard contradiction and the triangular-type standard contradiction. The results presented herein furnish the methodological basis for advancing contradiction-separation-based dynamic multi-clause automated deduction, thereby extending the expressive and deductive capabilities of automated reasoning systems beyond the classical binary paradigm.
- Abstract(参考訳): 信頼できるAIには、強力なだけでなく、透明性と信頼性を備えた推論システムが必要です。
ATP (Automated Theorem Proving) は形式的推論の中心であるが、古典的な二項分解は限定的であり、各ステップは2つの節のみを含み、ほとんどの2つのリテラルを排除している。
このボトルネックを克服するために、標準矛盾の概念と矛盾分離に基づく推論の理論が2018年に導入された。
本稿では,標準矛盾の体系的構築に焦点をあてて,その枠組みを推し進める。
具体的には,最大三角標準矛盾と三角標準矛盾という2つの主要な標準矛盾の手法について検討する。
これらの構造に基づいて,最大標準矛盾による節集合の満足度と不満足度を決定する手法を提案する。
さらに、最大三角形標準矛盾と三角型標準矛盾の両方に埋め込まれた標準部分矛盾の数を計算するための公式を導出する。
ここでは, 矛盾分離に基づく動的マルチクロース自動推論の方法論的基礎を整備し, 古典的二進パラダイムを超えて, 自動推論システムの表現的, 推論的能力を拡張した。
関連論文リスト
- Transfinite Fixed Points in Alpay Algebra as Ordinal Game Equilibria in Dependent Type Theory [0.0]
本稿では, 自己参照プロセスの安定な結果が, システムと環境との非有界リビジョン対話のユニークな平衡と同一であることを示すことによって, アルペイ・アルゲブラに寄与する。
固定点論、ゲームセマンティクス、順序解析、型理論から概念を統一することにより、この研究は無限の自己参照システムについての推論において、広くアクセス可能で形式的に厳密な基礎を確立する。
論文 参考訳(メタデータ) (2025-07-25T13:12:55Z) - Higher-Order Pattern Unification Modulo Similarity Relations [0.0]
高階理論とファジィ論理の組み合わせは意思決定に有用である。
我々は、よく確立された2つのコンポーネントと計算に精通したコンポーネントを統合することを目的とした、より簡単なアプローチを採用する。
本稿では,これらの類似性関係を変調する高次パターンの統一アルゴリズムを提案し,その終了,健全性,完全性を証明した。
論文 参考訳(メタデータ) (2025-07-17T15:18:22Z) - Soft Thinking: Unlocking the Reasoning Potential of LLMs in Continuous Concept Space [62.54887038032942]
ソフトシンキング(Soft Thinking)は、ソフトで抽象的な概念トークンを生成することによって、人間のような「ソフト」推論をエミュレートする訓練不要な手法である。
これらの概念トークンは、連続的な概念空間を形成するトークン埋め込みの確率重み付き混合によって生成される。
本質的に、生成された概念トークンは関連する離散トークンから複数の意味をカプセル化し、暗黙的に様々な推論経路を探索する。
論文 参考訳(メタデータ) (2025-05-21T17:29:15Z) - Polynomial-Time Relational Probabilistic Inference in Open Universes [14.312814866832804]
本稿では,使用する言語の表現力と推論による計算問題のトラクタビリティを両立させる一階確率推定手法を提案する。
具体的には、期待の2乗論理をリレーショナルセッティングに拡張する。
与えられた次数と大きさの証明によって証明可能な最も厳密な境界を導出し、固定度に対する2乗の総和の完全性を確立することができる。
論文 参考訳(メタデータ) (2025-05-07T04:14:03Z) - Fence Theorem: Towards Dual-Objective Semantic-Structure Isolation in Preprocessing Phase for 3D Anomaly Detection [32.44179060918441]
Fence Theoremは、前処理を二重目的意味的アイソレータとして定式化する。
Patch3Dは、Patch-CuttingとPatch-Matchingモジュールで構成され、セマンティック空間を分割し、類似のモジュールを統合する。
Anomaly-ShapeNetとReal3D-ADを異なる設定で実験した結果、前処理におけるよりきめ細かなセマンティックアライメントにより、ポイントレベルのAD精度が向上することが示された。
論文 参考訳(メタデータ) (2025-03-03T01:58:11Z) - Invariant Causal Set Covering Machines [48.169632766444906]
決定木のようなルールベースのモデルは、解釈可能な性質のために実践者にアピールする。
しかし、そのようなモデルを生成する学習アルゴリズムは、しばしば刺激的な関連に弱いため、因果関係の洞察を抽出することが保証されていない。
Invariant Causal Set Covering Machines は、古典的集合被覆マシンアルゴリズムの拡張であり、二値ルールの結合/分離を可能とし、スプリアス関係を確実に回避する。
論文 参考訳(メタデータ) (2023-06-07T20:52:01Z) - Understanding and Constructing Latent Modality Structures in Multi-modal
Representation Learning [53.68371566336254]
優れたパフォーマンスの鍵は、完全なモダリティアライメントではなく、有意義な潜在モダリティ構造にある、と我々は主張する。
具体的には,1)モダリティ内正規化のための深い特徴分離損失,2)モダリティ間正規化のためのブラウン橋損失,3)モダリティ内正規化およびモダリティ間正規化のための幾何学的整合損失を設計する。
論文 参考訳(メタデータ) (2023-03-10T14:38:49Z) - A contextually objective approach to the extended Wigner's friend
thought experiment [0.0]
エージェントがシステムと見なされるものや、そうでないものについて同意しなければならないと認める場合、矛盾は発生しないことを示す。
このような文脈的に客観的な量子力学のアプローチでは、明らかな矛盾が自動的に除去される。
論文 参考訳(メタデータ) (2023-01-08T10:58:02Z) - Tripartite Genuine Non-Gaussian Entanglement in Three-Mode Spontaneous
Parametric Downconversion [56.12820031986851]
2モードのSPDC相互作用の組み合わせによって生成される他のパラダイム的な3モードの絡み合い状態と異なる性質の3モードの絡み合いを持つ3モードの自然パラメトリックダウンコンバージョン相互作用によって生成される状態を示す。
論文 参考訳(メタデータ) (2020-01-20T10:39:28Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。