論文の概要: Automated Completion of Statements and Proofs in Synthetic Geometry: an
Approach based on Constraint Solving
- arxiv url: http://arxiv.org/abs/2401.11898v1
- Date: Mon, 22 Jan 2024 12:49:08 GMT
- ステータス: 処理完了
- システム内更新日: 2024-01-23 14:11:09.884380
- Title: Automated Completion of Statements and Proofs in Synthetic Geometry: an
Approach based on Constraint Solving
- Title(参考訳): 合成幾何学における文と証明の自動補完:制約解法に基づくアプローチ
- Authors: Salwa Tabet Gonzalez (University of Strasbourg), Predrag Jani\v{c}i\'c
(University of Belgrade), Julien Narboux (University of Strasbourg)
- Abstract要約: 不完全予想と不完全証明を完遂する枠組みを提案する。
このフレームワークは、不足した仮定を持つ予想を適切な定理に変えることができる。
また、提案したフレームワークは、人間の読みやすいマシンチェック可能な証明に証明スケッチを完成させるのに役立ちます。
- 参考スコア(独自算出の注目度): 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Conjecturing and theorem proving are activities at the center of mathematical
practice and are difficult to separate. In this paper, we propose a framework
for completing incomplete conjectures and incomplete proofs. The framework can
turn a conjecture with missing assumptions and with an under-specified goal
into a proper theorem. Also, the proposed framework can help in completing a
proof sketch into a human-readable and machine-checkable proof. Our approach is
focused on synthetic geometry, and uses coherent logic and constraint solving.
The proposed approach is uniform for all three kinds of tasks, flexible and, to
our knowledge, unique such approach.
- Abstract(参考訳): 導出と定理証明は数学的実践の中心にある活動であり、分離することは困難である。
本稿では,不完全予想と不完全証明を完遂する枠組みを提案する。
このフレームワークは、仮定が不足し、未特定の目標を持つ予想を適切な定理に変えることができる。
また、提案フレームワークは、証明スケッチを人間の可読かつ機械チェック可能な証明に仕上げるのに役立つ。
我々のアプローチは合成幾何学に重点を置いており、コヒーレント論理と制約解を用いる。
提案手法は,3種類のタスクすべてに対して柔軟で,私たちの知る限り,ユニークなアプローチである。
関連論文リスト
- Towards Automated Readable Proofs of Ruler and Compass Constructions [0.0]
本稿では,我々の三角形構成解法であるArgoTriCSが,一階述語論理とコヒーレント論理に対して,自動定理証明器とどのように協調するかを示す。
これらの証明は現在、多くの高いレベルの補題に依存しており、我々のゴールは、幾何の基本的な公理からそれら全てを正式に示すことである。
論文 参考訳(メタデータ) (2024-01-22T12:48:51Z) - An Encoding of Abstract Dialectical Frameworks into Higher-Order Logic [57.24311218570012]
このアプローチは抽象弁証法フレームワークのコンピュータ支援分析を可能にする。
応用例としては、メタ理論的性質の形式的解析と検証がある。
論文 参考訳(メタデータ) (2023-12-08T09:32:26Z) - Plan, Verify and Switch: Integrated Reasoning with Diverse X-of-Thoughts [65.15322403136238]
我々は,多種多様な推論の思考をLCMに促すことにより,総合的な問題解決フレームワーク XoT を提案する。
各質問に対して、XoTは常に最も適切なメソッドを選択して始まり、各メソッドを反復的に実行する。
各イテレーション内で、XoTは生成された回答の有効性を積極的にチェックし、外部エグゼクタからのフィードバックを取り入れます。
論文 参考訳(メタデータ) (2023-10-23T07:02:20Z) - ProofNet: Autoformalizing and Formally Proving Undergraduate-Level
Mathematics [7.607254619341369]
本稿では,学部レベルの数学の自己形式化と形式証明のためのベンチマークであるProofNetを紹介する。
ProofNetベンチマークは371の例で構成され、それぞれがLean 3.0の正式な定理文で構成されている。
テキスト内学習による文の自動書式化のベースライン結果について報告する。
論文 参考訳(メタデータ) (2023-02-24T03:28:46Z) - Geometric Methods for Sampling, Optimisation, Inference and Adaptive
Agents [102.42623636238399]
我々は,サンプリング,最適化,推論,適応的意思決定といった問題に根ざした基本的な幾何学的構造を同定する。
これらの問題を効率的に解くためにこれらの幾何学的構造を利用するアルゴリズムを導出する。
論文 参考訳(メタデータ) (2022-03-20T16:23:17Z) - A Formalisation of Abstract Argumentation in Higher-Order Logic [77.34726150561087]
本稿では,古典的高階論理へのエンコーディングに基づく抽象的議論フレームワークの表現手法を提案する。
対話型および自動推論ツールを用いた抽象的議論フレームワークのコンピュータ支援評価のための一様フレームワークを提供する。
論文 参考訳(メタデータ) (2021-10-18T10:45:59Z) - Logical Credal Networks [87.25387518070411]
本稿では,論理と確率を組み合わせた先行モデルの多くを一般化した表現的確率論的論理である論理的クレダルネットワークを紹介する。
本稿では,不確実性のあるマスターミンドゲームを解くこと,クレジットカード詐欺を検出することを含む,最大後部推論タスクの性能について検討する。
論文 参考訳(メタデータ) (2021-09-25T00:00:47Z) - TacticZero: Learning to Prove Theorems from Scratch with Deep
Reinforcement Learning [6.764610878007278]
深層強化学習を用いた対話型定理証明(ITP)の新しい手法を提案する。
我々は、各状態が潜在的な導出経路の集合を表すマルコフ決定プロセス(MDP)としてITPのプロセスを定式化する。
このフレームワークは、人間の専門家を使ったアプローチに匹敵するパフォーマンスを提供する。
論文 参考訳(メタデータ) (2021-02-19T06:08:39Z) - Prove-It: A Proof Assistant for Organizing and Verifying General
Mathematical Knowledge [0.0]
Prove-ItはPythonベースの汎用的対話型定理証明アシスタントである。
Prove-ItはフレキシブルなJupyterノートブックベースのユーザーインターフェイスを使って、対話や証明の手順を文書化している。
現在の開発と今後の研究には、量子回路操作と量子アルゴリズム検証への有望な応用が含まれている。
論文 参考訳(メタデータ) (2020-12-20T18:15:12Z) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳(メタデータ) (2020-02-17T16:06:02Z) - Geometric Formulation for Discrete Points and its Applications [0.0]
離散点上の幾何学の新しい定式化を導入する。
これは普遍微分計算に基づいており、関数の代数による離散集合の幾何学的記述を与える。
論文 参考訳(メタデータ) (2020-02-07T01:12:57Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。