論文の概要: Generating Compressed Combinatory Proof Structures -- An Approach to Automated First-Order Theorem Proving

• arxiv url: http://arxiv.org/abs/2209.12592v1
• Date: Mon, 26 Sep 2022 11:23:17 GMT
• ステータス: 処理完了
• システム内更新日: 2022-09-27 17:07:00.746318
• Title: Generating Compressed Combinatory Proof Structures -- An Approach to Automated First-Order Theorem Proving
• Title（参考訳）: Compressed Combinatory Proof Structures の生成 - 自動一階理論証明へのアプローチ
• Authors: Christoph Wernhard
• Abstract要約: ここでは、自動一階述語証明に対する「証明構造としての組合せ項」のアプローチを紹介する。 このアプローチは、凝縮した分枝に根付いた証明構造の項ビューと接続法に基づいて構築される。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Representing a proof tree by a combinator term that reduces to the tree lets subtle forms of duplication within the tree materialize as duplicated subterms of the combinator term. In a DAG representation of the combinator term these straightforwardly factor into shared subgraphs. To search for proofs, combinator terms can be enumerated, like clausal tableaux, interwoven with unification of formulas that are associated with nodes of the enumerated structures. To restrict the search space, the enumeration can be based on proof schemas defined as parameterized combinator terms. We introduce here this "combinator term as proof structure" approach to automated first-order proving, present an implementation and first experimental results. The approach builds on a term view of proof structures rooted in condensed detachment and the connection method. It realizes features known from the connection structure calculus, which has not been implemented so far.
• Abstract（参考訳）: ツリーに還元するコンビネータ項による証明木を表現することにより、ツリー内の微妙な形式の重複がコンビネータ項の重複部分項として実現される。 コンビネータのDAG表現では、これらは共有部分グラフに直結する。 証明を探索するために、コンビネータ項はクラウサル・タドーのように列挙され、列挙された構造のノードに関連付けられた公式の統一と織り交ぜられる。 探索空間を制限するために、列挙はパラメータ化コンビネータ項として定義された証明スキーマをベースとすることができる。 本稿では,この「証明構造としての組合せ項」アプローチを,一階の自動証明に導入し,実装と最初の実験結果を紹介する。 このアプローチは、凝縮剥離に根ざした証明構造の項ビューと接続法に基づいている。 これまで実装されていない接続構造計算から知られている特徴を実現する。

関連論文リスト

• Integrating Hierarchical Semantic into Iterative Generation Model for Entailment Tree Explanation [7.5496857647335585]
  本稿では,HiSCG (Controller-Generator) の枠組みに基づいて文の階層的意味論を統合するアーキテクチャを提案する。 提案手法はEntailmentBankデータセットの3つの設定で同等のパフォーマンスを実現する。
  論文  参考訳（メタデータ） (2024-09-26T11:46:58Z)
• Approximate learning of parsimonious Bayesian context trees [0.0]
  提案するフレームワークは、合成および実世界のデータ例に基づいてテストされる。 これは、実際のタンパク質配列やハニーポットコンピュータターミナルセッションに適合すると、既存のシーケンスモデルより優れている。
  論文  参考訳（メタデータ） (2024-07-27T11:50:40Z)
• Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
  本稿では, パール構造因果モデルにおいて, 因果関係などの部分的特定可能なクエリのバウンダリングの問題について議論する。 最近提案された反復EMスキームは初期化パラメータをサンプリングしてそれらの境界を内部近似する。 シンボルパラメータを実際の値に置き換えた回路構造を,単一のシンボル知識コンパイルによって得られることを示す。
  論文  参考訳（メタデータ） (2023-10-05T07:10:40Z)
• Interpretable Sequence Clustering [3.280979689839737]
  我々は、ISCT(Interpretable Sequence Clustering Tree)と呼ばれる手法を提案する。 ISCTは、k個のクラスタに対応するk個のリーフノードを生成し、各クラスタの生成方法に関する直感的な説明を提供する。 実世界の14のデータセットに対する実験結果から,本手法が解釈可能な木構造を提供することが示された。
  論文  参考訳（メタデータ） (2023-09-03T11:31:44Z)
• Range-Restricted Interpolation through Clausal Tableaux [0.0]
  一階述語論理の入力からクレイグの出力へ、範囲制限とホーン特性の変動がどのように受け継がれるかを示す。 証明システムは、一階ATPに由来するクラウスアル・タドーである。
  論文  参考訳（メタデータ） (2023-06-06T10:42:40Z)
• METGEN: A Module-Based Entailment Tree Generation Framework for Answer Explanation [59.33241627273023]
  複数のモジュールと推論コントローラを備えたモジュールベースのEntailment Tree GENフレームワークMETGENを提案する。 質問に対して、METGENは、別々のモジュールで単一ステップのエンタテインメントを実行し、コントローラで推論フローを選択することで、エンタテインメントツリーを反復的に生成することができる。 実験の結果,METGENは従来の最先端モデルよりも9%のパラメータで優れていた。
  論文  参考訳（メタデータ） (2022-05-05T12:06:02Z)
• Compositional Generalization Requires Compositional Parsers [69.77216620997305]
  直近のCOGSコーパスにおける構成原理によって導かれるシーケンス・ツー・シーケンスモデルとモデルを比較した。 構造一般化は構成一般化の重要な尺度であり、複雑な構造を認識するモデルを必要とする。
  論文  参考訳（メタデータ） (2022-02-24T07:36:35Z)
• A convergent inflation hierarchy for quantum causal structures [1.6758573326215689]
  因果構造は、確率変数間の関数的依存関係の記述である。 インフレ技術は因果構造を、ますます厳密な互換性テストの階層に関連付ける。 本稿では,量子インフレーション階層の最初のバージョンを構築する。
  論文  参考訳（メタデータ） (2021-10-27T18:00:02Z)
• Complex Event Forecasting with Prediction Suffix Trees: Extended Technical Report [70.7321040534471]
  複合イベント認識(CER)システムは、イベントのリアルタイムストリーム上のパターンを"即時"検出する能力によって、過去20年間に人気が高まっている。 このような現象が実際にCERエンジンによって検出される前に、パターンがいつ発生するかを予測する方法が不足している。 複雑なイベント予測の問題に対処しようとする形式的なフレームワークを提案する。
  論文  参考訳（メタデータ） (2021-09-01T09:52:31Z)
• Fold2Seq: A Joint Sequence(1D)-Fold(3D) Embedding-based Generative Model for Protein Design [70.27706384570723]
  Fold2Seqは特定の標的に条件付きタンパク質配列を設計するための新しいフレームワークである。 Fold2Seqの性能は, シーケンス設計の速度, カバレッジ, 信頼性において向上したか, 同等であったかを示す。 フォールドベースのFold2Seqの独特な利点は、構造ベースのディープモデルやRosettaDesignと比較して、3つの現実世界の課題においてより明確になる。
  論文  参考訳（メタデータ） (2021-06-24T14:34:24Z)
• Span-based Semantic Parsing for Compositional Generalization [53.24255235340056]
  SpanBasedSPは入力発話上のスパンツリーを予測し、部分的なプログラムが入力内のスパンをどのように構成するかを明示的に符号化する。 GeoQuery、SCAN、CLOSUREでは、SpanBasedSPはランダムスプリットの強いseq2seqベースラインと似ているが、構成一般化を必要とするスプリットのベースラインに比べて劇的に性能が向上する。
  論文  参考訳（メタデータ） (2020-09-13T16:42:18Z)

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

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