論文の概要: Learning from {\L}ukasiewicz and Meredith: Investigations into Proof
Structures (Extended Version)
- arxiv url: http://arxiv.org/abs/2104.13645v1
- Date: Wed, 28 Apr 2021 09:09:20 GMT
- ステータス: 処理完了
- システム内更新日: 2021-04-29 12:42:24.274338
- Title: Learning from {\L}ukasiewicz and Meredith: Investigations into Proof
Structures (Extended Version)
- Title(参考訳): L}ukasiewicz と Meredith から学ぶ:証明構造の研究(拡張版)
- Authors: Christoph Wernhard and Wolfgang Bibel
- Abstract要約: 本稿では,選択問題におけるグローバル特徴とその証明について検討する。
研究対象の課題は"axiom(s)"と" rule(s) imply goal(s)"の広義の形式である。
- 参考スコア(独自算出の注目度): 4.111899441919164
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: The material presented in this paper contributes to establishing a basis
deemed essential for substantial progress in Automated Deduction. It identifies
and studies global features in selected problems and their proofs which offer
the potential of guiding proof search in a more direct way. The studied
problems are of the wide-spread form of "axiom(s) and rule(s) imply goal(s)".
The features include the well-known concept of lemmas. For their elaboration
both human and automated proofs of selected theorems are taken into a close
comparative consideration. The study at the same time accounts for a coherent
and comprehensive formal reconstruction of historical work by {\L}ukasiewicz,
Meredith and others. First experiments resulting from the study indicate novel
ways of lemma generation to supplement automated first-order provers of various
families, strengthening in particular their ability to find short proofs.
- Abstract(参考訳): 本論文で提示された資料は,自動推論の実質的進歩に不可欠な基礎を確立するのに寄与する。
選択された問題のグローバル特徴と、より直接的な方法で証明探索を導く可能性を提供するそれらの証明を特定し、研究する。
研究された問題は、"axiom(s)" と " rule(s) imply goal(s)" の広義の形式である。
その特徴には、よく知られたレムマの概念が含まれる。
そのため、選択された定理の人間的証明と自動証明の両方が密接に比較検討される。
同時にこの研究は、キュカシエヴィチ、メレディスらによる歴史的著作の一貫性と包括的な形式的な再構築を論じている。
この研究から得られた最初の実験は、様々な家族の自動化された一階述語を補う新しい補題生成法を示し、特に短い証明を見つける能力を強化した。
関連論文リスト
- Seeing Unseen: Discover Novel Biomedical Concepts via
Geometry-Constrained Probabilistic Modeling [53.7117640028211]
同定された問題を解決するために,幾何制約付き確率的モデリング処理を提案する。
構成された埋め込み空間のレイアウトに適切な制約を課すために、重要な幾何学的性質のスイートを組み込む。
スペクトルグラフ理論法は、潜在的な新規クラスの数を推定するために考案された。
論文 参考訳(メタデータ) (2024-03-02T00:56:05Z) - Self-Convinced Prompting: Few-Shot Question Answering with Repeated
Introspection [13.608076739368949]
本稿では,大規模事前学習型言語モデルの可能性を活用する新しいフレームワークを提案する。
我々のフレームワークは、典型的な数発の連鎖プロンプトの出力を処理し、応答の正しさを評価し、回答を精査し、最終的には新しい解を生成する。
論文 参考訳(メタデータ) (2023-10-08T06:36:26Z) - Machine learning assisted exploration for affine Deligne-Lusztig
varieties [3.7863170254779335]
本稿では,ADLV(Affine Deligne-Lusztig variety)の幾何学を探索するために,機械学習支援フレームワークを活用した学際研究を提案する。
主な目的は, ADLVの既約成分の空白パターン, 寸法, 列挙について検討することである。
我々は、ある下界の次元に関する新たに特定された問題の完全な数学的証明を提供する。
論文 参考訳(メタデータ) (2023-08-22T11:12:53Z) - Rethinking Complex Queries on Knowledge Graphs with Neural Link
Predictors [65.56849255423866]
本稿では,証明可能な推論能力を備えた複雑なクエリを用いたエンドツーエンド学習を支援するニューラルシンボリック手法を提案する。
これまでに検討されていない10種類の新しいクエリを含む新しいデータセットを開発する。
提案手法は,新しいデータセットにおいて先行手法を著しく上回り,既存データセットにおける先行手法を同時に上回っている。
論文 参考訳(メタデータ) (2023-04-14T11:35:35Z) - Investigations into Proof Structures [2.7412662946127755]
我々は、証明をグローバルな方法で対象として操作し分析するための新しい形式論を導入し、詳述する。
これは、コヒーレントで包括的な形式的な再構築と、ルカシエヴィチによる広く研究されている問題の歴史的証明の分析に例示的に適用される。
論文 参考訳(メタデータ) (2023-02-14T12:29:39Z) - Full-Text Argumentation Mining on Scientific Publications [3.8754200816873787]
フルテキストSAMに対してADURとAREを組み合わせた逐次パイプラインモデルを提案する。
両サブタスクにおける事前学習言語モデル(PLM)の性能について,最初の解析を行った。
本稿では,非連続型ADUと談話コネクタの解釈が重要な課題であることを示す。
論文 参考訳(メタデータ) (2022-10-24T10:05:30Z) - Rethinking Bayesian Learning for Data Analysis: The Art of Prior and
Inference in Sparsity-Aware Modeling [20.296566563098057]
信号処理と機械学習のためのスパースモデリングは、20年以上にわたって科学研究の焦点となっている。
本稿では,3つの一般的なデータモデリングツールにスパーシティ・プロモーティング・プリエントを組み込むことの最近の進歩を概観する。
論文 参考訳(メタデータ) (2022-05-28T00:43:52Z) - Mapping Emulation for Knowledge Distillation [94.20630785525732]
本稿では,フェデレーション学習に不可欠なソース・ブラインド知識蒸留問題の定式化を行う。
新しいアーキテクチャMEKDを提案する。
様々なベンチマークにおいて、MEKDは既存のソースブレンドKD法より優れている。
論文 参考訳(メタデータ) (2022-05-21T02:38:16Z) - Evidentiality-guided Generation for Knowledge-Intensive NLP Tasks [59.761411682238645]
Retrieval-augmented Generation Modelは、多くの知識集約型NLPタスクにまたがって最先端のパフォーマンスを示している。
生成器の訓練に、パスが出力をサポートするための正しい証拠を含むか否かに関わらず、パスの明快さを組み込む方法を導入する。
論文 参考訳(メタデータ) (2021-12-16T08:18:47Z) - Alchemy: A structured task distribution for meta-reinforcement learning [52.75769317355963]
本稿では,構造的リッチネスと構造的透明性を組み合わせたメタRL研究のための新しいベンチマークを提案する。
Alchemyは3Dビデオゲームで、エピソードからエピソードまで手続き的に再サンプリングされる潜伏した因果構造を含んでいる。
本稿では,アルケミーの強力なRL剤について検討し,その1つについて詳細な分析を行った。
論文 参考訳(メタデータ) (2021-02-04T23:40:44Z) - Summarizing Text on Any Aspects: A Knowledge-Informed Weakly-Supervised
Approach [89.56158561087209]
文書に関連する任意の側面を要約する。
監視データがないため、我々は新しい弱い監督構築法とアスペクト・モデリング・スキームを開発した。
実験により,本手法は実文書と合成文書の両方を要約することで,性能の向上を図っている。
論文 参考訳(メタデータ) (2020-10-14T03:20:46Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。