Fugu-MT 論文翻訳(概要): Applying Second-Order Quantifier Elimination in Inspecting G\"odel's Ontological Proof

論文の概要: Applying Second-Order Quantifier Elimination in Inspecting G\"odel's Ontological Proof

arxiv url: http://arxiv.org/abs/2110.11108v1
Date: Thu, 21 Oct 2021 12:50:23 GMT
ステータス: 処理完了
システム内更新日: 2021-10-22 17:29:48.427418
Title: Applying Second-Order Quantifier Elimination in Inspecting G\"odel's Ontological Proof
Title（参考訳）: G\"odel's Ontological Proofにおける二階量子化器除去の適用
Authors: Christoph Wernhard
Abstract要約: フォーミュラマクロは複雑な公式やタスクを構成するのに使用される。 G"odelの存在論的証明とバリエーションは形式化され、自動ツールで分析される。
参考スコア（独自算出の注目度）: 0.0
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
Abstract: In recent years, G\"odel's ontological proof and variations of it were formalized and analyzed with automated tools in various ways. We supplement these analyses with a modeling in an automated environment based on first-order logic extended by predicate quantification. Formula macros are used to structure complex formulas and tasks. The analysis is presented as a generated type-set document where informal explanations are interspersed with pretty-printed formulas and outputs of reasoners for first-order theorem proving and second-order quantifier elimination. Previously unnoticed or obscured aspects and details of G\"odel's proof become apparent. Practical application possibilities of second-order quantifier elimination are shown and the encountered elimination tasks may serve as benchmarks.
Abstract（参考訳）: 近年、g\"odelのオントロジな証明とバリエーションは、様々な方法で自動化されたツールで形式化され、分析された。述語量化によって拡張された一階述語論理に基づく自動環境でのモデリングにより,これらの分析を補完する。式マクロは複雑な式やタスクを構成するために使われる。この分析は、非公式な説明と、一階定理証明と二階量子化器除去のための推論器の出力とが混在する生成されたタイプセット文書として提示される。以前は、G\"odel's proof の未確認あるいは曖昧な側面や詳細は明らかである。第2次量子化子除去の実用的な応用可能性を示し、遭遇した除去タスクがベンチマークとして機能する可能性がある。

関連論文リスト

"You Are An Expert Linguistic Annotator": Limits of LLMs as Analyzers of Abstract Meaning Representation [60.863629647985526]
文意味構造の解析において, GPT-3, ChatGPT, および GPT-4 モデルの成功と限界について検討した。モデルはAMRの基本形式を確実に再現でき、しばしばコアイベント、引数、修飾子構造をキャプチャできる。全体としては,これらのモデルではセマンティック構造の側面を捉えることができるが,完全に正確なセマンティック解析や解析をサポートする能力には重要な制限が残されている。
論文参考訳（メタデータ） (2023-10-26T21:47:59Z)
TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models [68.65075559137608]
本稿では, ATP ベンチマーク TRIGO を提案する。このベンチマークでは, ステップバイステップの証明で三角法式を縮小するだけでなく, 論理式上で生成する LM の推論能力を評価する。我々は、Webから三角法式とその縮小フォームを収集し、手作業で単純化プロセスに注釈を付け、それをリーン形式言語システムに翻訳する。我々はLean-Gymに基づく自動生成装置を開発し、モデルの一般化能力を徹底的に分析するために、様々な困難と分布のデータセット分割を作成する。
論文参考訳（メタデータ） (2023-10-16T08:42:39Z)
Mutual Exclusivity Training and Primitive Augmentation to Induce Compositionality [84.94877848357896]
最近のデータセットは、標準的なシーケンス・ツー・シーケンスモデルにおける体系的な一般化能力の欠如を露呈している。本稿では,セq2seqモデルの振る舞いを分析し,相互排他バイアスの欠如と全例を記憶する傾向の2つの要因を同定する。広範に使用されている2つの構成性データセット上で、標準的なシーケンス・ツー・シーケンスモデルを用いて、経験的改善を示す。
論文参考訳（メタデータ） (2022-11-28T17:36:41Z)
Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought [10.524051272257614]
大規模言語モデル(LLM)は、チェーン・オブ・シークレット・プロンプトが与えられた顕著な推論能力を示している。本稿では, PrOntoQAと呼ばれる合成質問応答データセットを提案し, それぞれの例を合成世界モデルとして生成する。これにより、生成された連鎖を形式解析の象徴的な証明に解析することができる。
論文参考訳（メタデータ） (2022-10-03T21:34:32Z)
Logical Satisfiability of Counterfactuals for Faithful Explanations in NLI [60.142926537264714]
本稿では, 忠実度スルー・カウンタファクトの方法論について紹介する。これは、説明に表される論理述語に基づいて、反実仮説を生成する。そして、そのモデルが表現された論理と反ファクトの予測が一致しているかどうかを評価する。
論文参考訳（メタデータ） (2022-05-25T03:40:59Z)
Sequential Learning of the Topological Ordering for the Linear Non-Gaussian Acyclic Model with Parametric Noise [6.866717993664787]
我々はDAGの因果順序を推定するための新しい逐次的アプローチを開発する。数千のノードを持つケースに対して,我々の手順がスケーラブルであることを示すための,広範な数値的証拠を提供する。
論文参考訳（メタデータ） (2022-02-03T18:15:48Z)
Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文参考訳（メタデータ） (2020-09-07T19:50:10Z)
Towards Concise, Machine-discovered Proofs of G\"odel's Two Incompleteness Theorems [3.222802562733787]
我々は、特異な論理に容易に適応したり、新たな推論プロセスを統合するように設計された、自動定理のための新しいフレームワークMATRを提案する。我々はMATRの高レベル設計と実装の詳細について説明する。次に、G"odelの不完全性定理の証明に適した形式化されたメタロジックを記述し、MATRにおける我々のメタロジックを用いて、第一不完全性定理と第二不完全性定理の両方の証明を半自動生成する進捗について報告する。
論文参考訳（メタデータ） (2020-05-06T03:29:34Z)
Generating Fact Checking Explanations [52.879658637466605]
まだ欠けているパズルの重要なピースは、プロセスの最も精巧な部分を自動化する方法を理解することです。本稿では、これらの説明を利用可能なクレームコンテキストに基づいて自動生成する方法について、最初の研究を行う。この結果から,個別に学習するのではなく,両目標を同時に最適化することで,事実確認システムの性能が向上することが示唆された。
論文参考訳（メタデータ） (2020-04-13T05:23:25Z)
Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic [0.0]
PIEは、一階述語論理に基づく自動推論のためのProlog組み込み環境である。マクロ定義、推論の呼び出し、フォームトされた自然言語テキストにまたがるドキュメントに基づいたワークフローをサポートする。
論文参考訳（メタデータ） (2020-02-24T16:09:10Z)

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