論文の概要: Towards Automated Readable Proofs of Ruler and Compass Constructions
- arxiv url: http://arxiv.org/abs/2401.13700v1
- Date: Mon, 22 Jan 2024 12:48:51 GMT
- ステータス: 処理完了
- システム内更新日: 2024-01-26 17:02:45.069195
- Title: Towards Automated Readable Proofs of Ruler and Compass Constructions
- Title(参考訳): 定規とコンパス構成の自動可読証明に向けて
- Authors: Vesna Marinkovi\'c (Faculty of Mathematics, University of Belgrade),
Tijana \v{S}ukilovi\'c (Faculty of Mathematics, University of Belgrade),
Filip Mari\'c (Faculty of Mathematics, University of Belgrade)
- Abstract要約: 本稿では,我々の三角形構成解法であるArgoTriCSが,一階述語論理とコヒーレント論理に対して,自動定理証明器とどのように協調するかを示す。
これらの証明は現在、多くの高いレベルの補題に依存しており、我々のゴールは、幾何の基本的な公理からそれら全てを正式に示すことである。
- 参考スコア(独自算出の注目度): 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Although there are several systems that successfully generate construction
steps for ruler and compass construction problems, none of them provides
readable synthetic correctness proofs for generated constructions. In the
present work, we demonstrate how our triangle construction solver ArgoTriCS can
cooperate with automated theorem provers for first order logic and coherent
logic so that it generates construction correctness proofs, that are both
human-readable and formal (can be checked by interactive theorem provers such
as Coq or Isabelle/HOL). These proofs currently rely on many high-level lemmas
and our goal is to have them all formally shown from the basic axioms of
geometry.
- Abstract(参考訳): 定規およびコンパス構築問題に対する構築手順をうまく生成するシステムはいくつか存在するが、いずれも生成した構成に対して可読な合成正しさ証明を提供していない。
本研究は,我々の三角形構成解法であるArgoTriCSが一階述語論理とコヒーレント論理の自動定理証明と協調して,人間の可読性および形式性の両方を持つ構成正当性証明(CoqやIsabelle/HOLのような対話的定理証明によって検証できる)を生成する方法を示す。
これらの証明は現在、多くの高いレベルの補題に依存しており、我々の目標は、幾何の基本的な公理からそれらを全て正式に示すことである。
関連論文リスト
- MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [88.72298746872396]
MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。
5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。
我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
論文 参考訳(メタデータ) (2024-02-14T05:57:58Z) - Automated Completion of Statements and Proofs in Synthetic Geometry: an
Approach based on Constraint Solving [0.0]
不完全予想と不完全証明を完遂する枠組みを提案する。
このフレームワークは、不足した仮定を持つ予想を適切な定理に変えることができる。
また、提案したフレームワークは、人間の読みやすいマシンチェック可能な証明に証明スケッチを完成させるのに役立ちます。
論文 参考訳(メタデータ) (2024-01-22T12:49:08Z) - Query Structure Modeling for Inductive Logical Reasoning Over Knowledge
Graphs [67.043747188954]
KGに対する帰納的論理的推論のための構造モデル付きテキスト符号化フレームワークを提案する。
線形化されたクエリ構造とエンティティを、事前訓練された言語モデルを使ってエンコードして、回答を見つける。
2つの帰納的論理推論データセットと3つの帰納的推論データセットについて実験を行った。
論文 参考訳(メタデータ) (2023-05-23T01:25:29Z) - Towards Autoformalization of Mathematics and Code Correctness:
Experiments with Elementary Proofs [5.045988012508899]
オートフォーマル化(Autoformalization)は、自然言語で書かれた証明を、対話的定理証明を通じてコンピュータで検証可能な形式表現に変換することによって、この問題に対処しようとする。
本稿では, 基本数学的証明を, Coq の対話的定理証明器の言語における等価な形式化に変換する, ユニバーサルトランスフォーマーアーキテクチャに基づく意味解析手法を提案する。
論文 参考訳(メタデータ) (2023-01-05T17:56:00Z) - Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal
Proofs [30.57062828812679]
本稿では,形式的証明スケッチに非公式な証明をマッピングするDraft, Sketch, Prove(DSP)を紹介する。
大規模言語モデルでは,形式的証明と同じ推論手順を踏襲して,構造化された形式的スケッチを作成可能であることを示す。
論文 参考訳(メタデータ) (2022-10-21T22:37:22Z) - Generating Compressed Combinatory Proof Structures -- An Approach to
Automated First-Order Theorem Proving [0.0]
ここでは、自動一階述語証明に対する「証明構造としての組合せ項」のアプローチを紹介する。
このアプローチは、凝縮した分枝に根付いた証明構造の項ビューと接続法に基づいて構築される。
論文 参考訳(メタデータ) (2022-09-26T11:23:17Z) - Generating Natural Language Proofs with Verifier-Guided Search [74.9614610172561]
NLProofS (Natural Language Proof Search) を提案する。
NLProofSは仮説に基づいて関連するステップを生成することを学習する。
EntailmentBank と RuleTaker の最先端のパフォーマンスを実現している。
論文 参考訳(メタデータ) (2022-05-25T02:22:30Z) - Fold2Seq: A Joint Sequence(1D)-Fold(3D) Embedding-based Generative Model
for Protein Design [70.27706384570723]
Fold2Seqは特定の標的に条件付きタンパク質配列を設計するための新しいフレームワークである。
Fold2Seqの性能は, シーケンス設計の速度, カバレッジ, 信頼性において向上したか, 同等であったかを示す。
フォールドベースのFold2Seqの独特な利点は、構造ベースのディープモデルやRosettaDesignと比較して、3つの現実世界の課題においてより明確になる。
論文 参考訳(メタデータ) (2021-06-24T14:34:24Z) - Inter-GPS: Interpretable Geometry Problem Solving with Formal Language
and Symbolic Reasoning [123.06420835072225]
3,002の幾何学的問題と密接なアノテーションを形式言語に含む新しい大規模ベンチマークGeometry3Kを構築します。
我々は、Interpretable Geometry Problemsolvr (Inter-GPS)と呼ばれる形式言語と記号推論を用いた新しい幾何学的解法を提案する。
イントラGPSは定理の知識を条件付き規則として取り入れ、記号的推論を段階的に行う。
論文 参考訳(メタデータ) (2021-05-10T07:46:55Z) - Automating the Generation of High School Geometry Proofs using Prolog in
an Educational Context [0.0]
我々は、Prologのエンコーディングから証明の完全なセットの生成に至るまで、我々が実装した中核的な概念を提示する。
また、私たちが直面した主な問題と、選択したソリューションも提示します。
論文 参考訳(メタデータ) (2020-02-28T05:23:16Z) - Learning to Prove Theorems by Learning to Generate Theorems [71.46963489866596]
我々は、定理証明器を訓練するために、定理と証明を自動的に合成するニューラルジェネレータを学習する。
実世界の課題に関する実験は、我々の手法による合成データが定理証明器を改善することを示した。
論文 参考訳(メタデータ) (2020-02-17T16:06:02Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。