論文の概要: A Rule Based Theorem Prover: an Introduction to Proofs in Secondary Schools

• arxiv url: http://arxiv.org/abs/2303.05863v1
• Date: Fri, 10 Mar 2023 11:36:10 GMT
• ステータス: 処理完了
• システム内更新日: 2023-03-13 15:11:31.042226
• Title: A Rule Based Theorem Prover: an Introduction to Proofs in Secondary Schools
• Title（参考訳）: ルールに基づく理論証明:中等教育における証明の紹介
• Authors: Joana Teles (CMUC / Department of Mathematics, University of Coimbra), Vanda Santos (CIDTFF, University of Aveiro and CISUC), Pedro Quaresma (CISUC / Department of Mathematics, University of Coimbra)
• Abstract要約: 中学校における自動推論システムの導入は、いくつかのボトルネックに直面している。 幾何学的自動定理プローバーの結果と学校での推論と証明の通常の実践との間の不一致は、教育環境においてそのようなツールを広く使用する上で大きな障壁となる。 授業計画が提示され、その目標は幾何学的定理を証明する公式なデモンストレーションの導入であり、その目標に学生を動機付けようとすることである。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The introduction of automated deduction systems in secondary schools face several bottlenecks. Beyond the problems related with the curricula and the teachers, the dissonance between the outcomes of the geometry automated theorem provers and the normal practice of conjecturing and proving in schools is a major barrier to a wider use of such tools in an educational environment. Since the early implementations of geometry automated theorem provers, applications of artificial intelligence methods, synthetic provers based on inference rules and using forward chaining reasoning are considered to be more suited for education proposes. Choosing an appropriate set of rules and an automated method that can use those rules is a major challenge. We discuss one such rule set and its implementation using the geometry deductive databases method (GDDM). The approach is tested using some chosen geometric conjectures that could be the goal of a 7th year class (approx. 12-year-old students). A lesson plan is presented, its goal is the introduction of formal demonstration of proving geometric theorems, trying to motivate students to that goal
• Abstract（参考訳）: 中学校における自動推論システムの導入はいくつかのボトルネックに直面している。 カリキュラムと教師に関する問題以外にも、幾何学的自動定理プローバーの結果と学校での推論と証明の通常の実践との間の不一致は、教育環境においてそのようなツールを広く使用する上で大きな障壁となる。 幾何自動定理プローバーの初期実装以降、人工知能の応用、推論規則に基づく合成プローバー、前方連鎖推論の利用は、より教育的提案に適していると考えられる。 適切なルールセットの選択と、それらのルールを使用できる自動化メソッドは、大きな課題です。 本稿では,幾何帰納的データベース法(GDDM)を用いて,そのようなルールセットとその実装について論じる。 このアプローチは、7年生(約12歳の学生)の目標となる幾何予想を使ってテストされる。 授業計画が提示され、その目標は、学生をその目標に動機付けようとする幾何学的定理を証明する公式なデモンストレーションの導入である。

関連論文リスト

• Fuse, Reason and Verify: Geometry Problem Solving with Parsed Clauses from Diagram [78.79651421493058]
  平面幾何学的問題解法 (PGPS) のニューラルネットワークモデルを提案し, モーダル融合, 推論過程, 知識検証の3つの重要なステップについて述べる。 推論のために、幾何学的推論過程を記述するための説明可能な解プログラムを設計し、自己限定デコーダを用いて解プログラムを自動回帰的に生成する。 また, PGPS9Kと呼ばれる大規模幾何学的問題データセットを構築し, テキスト節, 解法プログラム, 関連知識解決器の詳細なアノテーションを含む。
  論文  参考訳（メタデータ） (2024-07-10T02:45:22Z)
• Autoformalizing Euclidean Geometry [74.72212706513318]
  ユークリッド幾何学の自己形式化のためのニューロシンボリックフレームワークを提案する。 1つの課題は、非公式な証明が図に頼り、形式化が難しいテキストのギャップを残すことである。 自己形式化定理文の自動意味評価を行う。
  論文  参考訳（メタデータ） (2024-05-27T14:35:10Z)
• Learning to Solve Geometry Problems via Simulating Human Dual-Reasoning Process [84.49427910920008]
  近年,幾何学的問題解決 (GPS) が注目されている。 解法は、テキストとダイアグラムの両方を包括的に理解し、重要な幾何学的知識を習得し、推論に適切に適用する必要がある。 既存の研究は、ニューラルネットワーク翻訳のパラダイムに従っており、人間の幾何学的推論の本質的な特徴を無視したエンコーダの能力の向上にのみ焦点をあてている。
  論文  参考訳（メタデータ） (2024-05-10T03:53:49Z)
• Automated Completion of Statements and Proofs in Synthetic Geometry: an Approach based on Constraint Solving [0.0]
  不完全予想と不完全証明を完遂する枠組みを提案する。 このフレームワークは、不足した仮定を持つ予想を適切な定理に変えることができる。 また、提案したフレームワークは、人間の読みやすいマシンチェック可能な証明に証明スケッチを完成させるのに役立ちます。
  論文  参考訳（メタデータ） (2024-01-22T12:49:08Z)
• Open Geometry Prover Community Project [0.0]
  Open Geometry Prover Community Projectは、共通な"umbrella"の下で、幾何自動定理プロバーの開発のための様々な取り組みを統合することを目的としている。 本稿では、そのような統合に必要なステップと、これらのステップの現在の実装について説明する。
  論文  参考訳（メタデータ） (2022-01-03T09:27:23Z)
• 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)
• Generative Language Modeling for Automated Theorem Proving [94.01137612934842]
  この研究は、自動定理プロバーの人間に対する大きな制限が言語モデルから生成することで対処できる可能性によって動機づけられている。 本稿ではメタマス形式化言語のための自動証明と証明アシスタント GPT-f を提案し,その性能を解析する。
  論文  参考訳（メタデータ） (2020-09-07T19:50:10Z)
• Towards a Geometry Automated Provers Competition [0.0]
  GATPの競争により、GATP開発者が既存のものを改善し、新しいものを提案するためのテストベンチを作成することができる。 また、特定の用途に最適な実装を選択するために、"クライアント"(例えば教育用eラーニングシステムの開発者)が使用可能なGATPのランキングを確立することもできる。
  論文  参考訳（メタデータ） (2020-02-28T05:24:29Z)
• 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)

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

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。