論文の概要: Deriving Theorems in Implicational Linear Logic, Declaratively
- arxiv url: http://arxiv.org/abs/2009.10241v1
- Date: Tue, 22 Sep 2020 00:48:45 GMT
- ステータス: 処理完了
- システム内更新日: 2022-10-15 23:20:17.517608
- Title: Deriving Theorems in Implicational Linear Logic, Declaratively
- Title（参考訳）: 含意線形論理における定理の導出
- Authors: Paul Tarau (University of North Texas), Valeria de Paiva (Topos
Institute)
- Abstract要約: 命題直観主義線形論理の含意的断片において、与えられた大きさのすべての定理を生成する方法を示す。
応用として、線形論理定理証明器の正確性とスケーラビリティ試験のためのデータセットを生成し、定理証明問題に取り組むニューラルネットワークのトレーニングデータを生成する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: The problem we want to solve is how to generate all theorems of a given size
in the implicational fragment of propositional intuitionistic linear logic. We
start by filtering for linearity the proof terms associated by our Prolog-based
theorem prover for Implicational Intuitionistic Logic. This works, but using
for each formula a PSPACE-complete algorithm limits it to very small formulas.
We take a few walks back and forth over the bridge between proof terms and
theorems, provided by the Curry-Howard isomorphism, and derive step-by-step an
efficient algorithm requiring a low polynomial effort per generated theorem.
The resulting Prolog program runs in O(N) space for terms of size N and
generates in a few hours 7,566,084,686 theorems in the implicational fragment
of Linear Intuitionistic Logic together with their proof terms in normal form.
As applications, we generate datasets for correctness and scalability testing
of linear logic theorem provers and training data for neural networks working
on theorem proving challenges. The results in the paper, organized as a
literate Prolog program, are fully replicable.
Keywords: combinatorial generation of provable formulas of a given size,
intuitionistic and linear logic theorem provers, theorems of the implicational
fragment of propositional linear intuitionistic logic, Curry-Howard
isomorphism, efficient generation of linear lambda terms in normal form, Prolog
programs for lambda term generation and theorem proving.
- Abstract（参考訳）: 私たちが解決したい問題は、命題直観主義線形論理の含意的断片において、与えられた大きさのすべての定理を生成する方法である。
まず、Implicational Intuitionistic Logic の Prolog-based theorem proofr に付随する証明項を線形性のためにフィルタリングする。
これは機能するが、各公式にpspace完全アルゴリズムを用いることで、非常に小さな公式に制限される。
証明項と定理の間の橋渡しを、カリー・ホワード同型(英語版)によって提供され、生成定理ごとに低い多項式労力を必要とする効率的なアルゴリズムをステップ・バイ・ステップで導出する。
結果のPrologプログラムはサイズ N の条件で O(N) 空間で実行され、線形直観主義論理(英語版)の含意的な断片における時間 7,566,084,686 の定理とそれらの証明項を正規形式で生成する。
応用として,線形論理定理の精度と拡張性をテストするためのデータセットを生成し,定理証明の課題に取り組むニューラルネットワークのトレーニングデータを生成する。
論文の成果は、リテラトPrologプログラムとして整理され、完全に複製可能である。
キーワード:与えられた大きさの証明可能な公式の組合せ生成、直観主義的および線形論理定理の証明、命題的線形直観主義論理の含意的断片の定理、カレーホワード同型、正規形における線形ラムダ項の効率的な生成、ラムダ項生成および定理証明のためのprologプログラム。
関連論文リスト
- Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation [71.32761934724867]
この研究は、記号的突然変異を通じて形式的な定理を構成するデータ合成のフレームワークであるAlchemyを提案する。
マドリブにおける各候補定理について、書き直しや適用に使用できるすべてのイベーシブルな定理を同定する。
その結果、マドリブの定理の数は110kから6Mへと桁違いに増加する。
論文 参考訳（メタデータ） (2024-10-21T08:04:21Z) - Proving Theorems Recursively [80.42431358105482]
本稿では、定理をレベル・バイ・レベルで証明するPOETRYを提案する。
従来のステップバイステップメソッドとは異なり、POETRYは各レベルで証明のスケッチを検索する。
また,POETRYが検出した最大証明長は10～26。
論文 参考訳（メタデータ） (2024-05-23T10:35:08Z) - ATG: Benchmarking Automated Theorem Generation for Generative Language Models [83.93978859348313]
人間はより広範に複雑な数学的結果を探求するために新しい定理を開発することができる。
現在の生成言語モデル(LM)は、定理の自動証明において著しく改善されている。
本稿では,エージェントが価値ある(あるいは新しい)定理を自動生成できるかどうかを評価する自動定理生成ベンチマークを提案する。
論文 参考訳（メタデータ） (2024-05-05T02:06:37Z) - LeanReasoner: Boosting Complex Logical Reasoning with Lean [19.486080494198724]
大規模言語モデル(LLM)は、論理的不整合とそのような推論の固有の難しさのために、複雑な論理的推論に苦しむことが多い。
これらの課題に対処するために、定理実証フレームワークであるLeanを使用します。
論理的推論問題をリーン内の定理にフォーマルにすることで、対応する定理を証明または証明することで、それらを解決することができる。
論文 参考訳（メタデータ） (2024-03-20T05:29:06Z) - LINC: A Neurosymbolic Approach for Logical Reasoning by Combining
Language Models with First-Order Logic Provers [60.009969929857704]
論理的推論は、科学、数学、社会に潜在的影響を与える可能性のある人工知能にとって重要なタスクである。
本研究では、LINCと呼ばれるモジュール型ニューロシンボリックプログラミングのようなタスクを再構成する。
我々は,FOLIOとProofWriterのバランスの取れたサブセットに対して,ほぼすべての実験条件下で,3つの異なるモデルに対して顕著な性能向上を観察した。
論文 参考訳（メタデータ） (2023-10-23T17:58:40Z) - Linear Temporal Logic Modulo Theories over Finite Traces (Extended
Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。
命題の文字は任意の理論で解釈された一階述語式に置き換えられる。
Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文 参考訳（メタデータ） (2022-04-28T17:57:33Z) - Neural Unification for Logic Reasoning over Natural Language [0.28675177318965034]
自動定理証明(Automated Theorem Proving)は、いくつかの予想(クエリ)が一連の公理(事実と規則)の論理的な結果であることを示すことができるコンピュータプログラムの開発を扱う。
近年のアプローチでは、自然言語(英語)で表される公理の予想を導出するトランスフォーマーに基づくアーキテクチャが提案されている。
本研究は, 一般化の項における最先端結果を実現するニューラルユニファイザという, 新たなアーキテクチャを提案する。
論文 参考訳（メタデータ） (2021-09-17T10:48:39Z) - Neural Proof Nets [0.8379286663107844]
本稿では,Sinkhorn ネットワークをベースとした証明ネットのニューラルバリアントを提案する。
AEThelでは,テキスト文の正しい書き起こしを線形ラムダ計算の証明や用語として70%の精度で行うことができる。
論文 参考訳（メタデータ） (2020-09-26T22:48:47Z) - Partial Orders, Residuation, and First-Order Linear Logic [0.20305676256390934]
各列の先行式上の一意線型順序を定義するような部分順序制約を加えることで、多くの有用な論理作用素を定義できることを示す。
論文 参考訳（メタデータ） (2020-08-14T13:06:21Z) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳（メタデータ） (2020-02-17T16:06:02Z) - An Experimental Study of Formula Embeddings for Automated Theorem
Proving in First-Order Logic [13.633012068936894]
本研究では,一般的なグラフベースエンコーディングを持つ現行システムに適用されるパターンベースの埋め込みについて,実験的に比較する。
実験により、より複雑なグラフベースの埋め込みにより、より単純な実行時の符号化方式の利点が打ち消されることが示された。
論文 参考訳（メタデータ） (2020-02-02T16:07:15Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。