論文の概要: Automated Planning Techniques for Elementary Proofs in Abstract Algebra
- arxiv url: http://arxiv.org/abs/2312.06490v1
- Date: Mon, 11 Dec 2023 16:17:43 GMT
- ステータス: 処理完了
- システム内更新日: 2023-12-12 14:52:21.056087
- Title: Automated Planning Techniques for Elementary Proofs in Abstract Algebra
- Title(参考訳): 抽象代数における初等証明の自動計画手法
- Authors: Alice Petrov, Christian Muise
- Abstract要約: 抽象代数学における基本証明を構築するための計画法について検討する。
我々は、決定論的領域と非決定論的領域の両方において、基本的な意味、平等、および規則を実装している。
この初期実装の成功は、自動計画で見られる確立されたテクニックが、比較的新しい自動定理証明分野に適用可能であることを示唆している。
- 参考スコア(独自算出の注目度): 5.379968204052965
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: This paper explores the application of automated planning to automated
theorem proving, which is a branch of automated reasoning concerned with the
development of algorithms and computer programs to construct mathematical
proofs. In particular, we investigate the use of planning to construct
elementary proofs in abstract algebra, which provides a rigorous and axiomatic
framework for studying algebraic structures such as groups, rings, fields, and
modules. We implement basic implications, equalities, and rules in both
deterministic and non-deterministic domains to model commutative rings and
deduce elementary results about them. The success of this initial
implementation suggests that the well-established techniques seen in automated
planning are applicable to the relatively newer field of automated theorem
proving. Likewise, automated theorem proving provides a new, challenging domain
for automated planning.
- Abstract(参考訳): 本稿では, 自動定理証明への自動計画の適用について検討する。これは, 数学的証明を構築するためのアルゴリズムとコンピュータプログラムの開発に関する自動推論の一分野である。
特に, 群, 環, 体, 加群といった代数構造を研究するための厳密で公理的な枠組みを提供する抽象代数学における初等的証明を構築するための計画法の使用について検討する。
我々は、可換環をモデル化し、それらの基本的な結果を推測するために、決定論的および非決定論的領域の両方に基本的な意味、等性、規則を実装する。
この初期実装の成功は、自動化計画に見られる確立されたテクニックが、比較的新しい自動定理証明分野に適用可能であることを示唆している。
同様に、自動定理証明は、自動計画のための新しい挑戦的な領域を提供する。
関連論文リスト
- A Neural Rewriting System to Solve Algorithmic Problems [51.485598133884615]
本稿では,特殊なモジュールで構成されたニューラルアーキテクチャとして,書き換えシステムを実装可能であることを示す。
シンボリック・フォーミュラの簡素化を必要とする3種類のアルゴリズムタスクに対して,本モデルの評価を行った。
論文 参考訳(メタデータ) (2024-02-27T10:57:07Z) - A Hybrid System for Systematic Generalization in Simple Arithmetic
Problems [70.91780996370326]
本稿では,記号列に対する合成的および体系的推論を必要とする算術的問題を解くことができるハイブリッドシステムを提案する。
提案システムは,最も単純なケースを含むサブセットでのみ訓練された場合においても,ネストした数式を正確に解くことができることを示す。
論文 参考訳(メタデータ) (2023-06-29T18:35:41Z) - Connecting Proof Theory and Knowledge Representation: Sequent Calculi
and the Chase with Existential Rules [1.8275108630751844]
実存則の文脈におけるチェイス機構は、本質的には、一階述語論理に対するゲンツェンの逐次計算の拡張における証明探索と同じであることを示す。
我々は、決定可能性の証明を理論的に確立するための中央ツールを、知識表現の文脈において、決定可能性の中央ツールと正式に結合する。
論文 参考訳(メタデータ) (2023-06-05T01:10:23Z) - Reformulation Techniques for Automated Planning: A Systematic Review [4.83420384410068]
ドメインに依存しない計画の基盤は、計画ロジックと知識モデルとの分離である。
過去数十年にわたり、改革技術の設計に多大な研究努力が注がれている。
本稿では,古典的計画の改革手法に関する大規模研究の体系的なレビューを行う。
論文 参考訳(メタデータ) (2023-01-24T15:33:37Z) - Structural Analysis of Branch-and-Cut and the Learnability of Gomory
Mixed Integer Cuts [88.94020638263467]
ブランチ・アンド・カット(ブランチ・アンド・カット)として知られる分岐・アンド・バウンドアルゴリズムにおける切断平面の組み入れは、現代の整数計画解法のバックボーンを形成する。
入力整数プログラムに付加される切断平面を定義するパラメータの変化により、アルゴリズムの各ステップがどのように影響を受けるかをピン留めする、分岐切断の新たな構造解析を行う。
この分析の主な応用は、機械学習を用いてブランチ・アンド・カット時にどの切断面を適用するかを決定するためのサンプルの複雑性保証を導出することである。
論文 参考訳(メタデータ) (2022-04-15T03:32:40Z) - Goal Agnostic Planning using Maximum Likelihood Paths in Hypergraph
World Models [1.370633147306388]
本稿では,ハイパーグラフに基づく機械学習アルゴリズム,データ構造駆動型メンテナンス手法,およびDijkstraのアルゴリズムの確率的応用に基づく計画アルゴリズムを提案する。
このアルゴリズムが問題空間内の最適解を決定すること、数学的に有界な学習性能を証明し、時間を通してシステム状態の進行を解析する数学的モデルを提供する。
論文 参考訳(メタデータ) (2021-10-18T16:22:33Z) - Refining Labelled Systems for Modal and Constructive Logics with
Applications [0.0]
この論文は、モーダル論理や構成論理のセマンティクスを「経済的な」証明システムに変換する手段として機能する。
精製法は、ラベル付きおよびネストされたシーケント計算の2つの証明理論パラダイムを結合する。
導入された洗練されたラベル付き電卓は、デオン性STIT論理に対する最初の証明探索アルゴリズムを提供するために使用される。
論文 参考訳(メタデータ) (2021-07-30T08:27:15Z) - Induction and Exploitation of Subgoal Automata for Reinforcement
Learning [75.55324974788475]
本稿では,Regressed Learning (RL)タスクにおけるサブゴールの学習と活用のためのISAを提案する。
ISAは、タスクのサブゴールによってエッジがラベル付けされたオートマトンであるサブゴールオートマトンを誘導することで強化学習をインターリーブする。
サブゴールオートマトンはまた、タスクの完了を示す状態と、タスクが成功せずに完了したことを示す状態の2つの特別な状態で構成されている。
論文 参考訳(メタデータ) (2020-09-08T16:42:55Z) - Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。
本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
論文 参考訳(メタデータ) (2020-09-07T19:50:10Z) - A General Framework for Consistent Structured Prediction with Implicit
Loss Embeddings [113.15416137912399]
構造化予測のための理論的・アルゴリズム的な枠組みを提案し,解析する。
問題に対して適切な幾何を暗黙的に定義する、損失関数の大規模なクラスについて検討する。
出力空間を無限の濃度で扱うとき、推定子の適切な暗黙の定式化が重要であることが示される。
論文 参考訳(メタデータ) (2020-02-13T10:30:04Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。