論文の概要: 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歳の学生)の目標となる幾何予想を使ってテストされる。
授業計画が提示され、その目標は、学生をその目標に動機付けようとする幾何学的定理を証明する公式なデモンストレーションの導入である。
関連論文リスト
- Automated Completion of Statements and Proofs in Synthetic Geometry: an
Approach based on Constraint Solving [0.0]
不完全予想と不完全証明を完遂する枠組みを提案する。
このフレームワークは、不足した仮定を持つ予想を適切な定理に変えることができる。
また、提案したフレームワークは、人間の読みやすいマシンチェック可能な証明に証明スケッチを完成させるのに役立ちます。
論文 参考訳(メタデータ) (2024-01-22T12:49:08Z) - TheoremQA: A Theorem-driven Question Answering dataset [100.39878559382694]
GPT-4のこれらの問題を解決する能力は非並列であり、Program-of-Thoughts Promptingの精度は51%である。
TheoremQAは、350の定理をカバーする800の高品質な質問を含むドメインの専門家によってキュレートされる。
論文 参考訳(メタデータ) (2023-05-21T17:51:35Z) - UniGeo: Unifying Geometry Logical Reasoning via Reformulating
Mathematical Expression [127.68780714438103]
計算と証明の2つの主要な幾何学問題は、通常2つの特定のタスクとして扱われる。
我々は4,998の計算問題と9,543の証明問題を含むUniGeoという大規模統一幾何問題ベンチマークを構築した。
また,複数タスクの幾何変換フレームワークであるGeoformerを提案し,計算と証明を同時に行う。
論文 参考訳(メタデータ) (2022-12-06T04:37:51Z) - Open Geometry Prover Community Project [0.0]
Open Geometry Prover Community Projectは、共通な"umbrella"の下で、幾何自動定理プロバーの開発のための様々な取り組みを統合することを目的としている。
本稿では、そのような統合に必要なステップと、これらのステップの現在の実装について説明する。
論文 参考訳(メタデータ) (2022-01-03T09:27:23Z) - GeoQA: A Geometric Question Answering Benchmark Towards Multimodal
Numerical Reasoning [172.36214872466707]
我々は、テキスト記述、視覚図、定理知識の包括的理解を必要とする幾何学的問題を解くことに注力する。
そこで本研究では,5,010の幾何学的問題を含む幾何学的質問応答データセットGeoQAを提案する。
論文 参考訳(メタデータ) (2021-05-30T12:34:17Z) - 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) - Using Automated Theorem Provers for Mistake Diagnosis in the Didactics
of Mathematics [0.0]
Diproche システムは、Koepke や Schr"oder 、 Cramer などによる Naproche システムに似た初心者学生の運動の文脈に特化している。
本稿では,このようなアンチATPの概念を簡潔に解説し,その実装における基本技術について解説する。
論文 参考訳(メタデータ) (2020-02-12T16:36:59Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。