A Rule Based Theorem Prover: an Introduction to Proofs in Secondary Schools

要約

中等学校における自動控除システムの導入は、いくつかのボトルネックに直面しています。
カリキュラムと教師に関連する問題を超えて、幾何学の自動定理証明器の結果と、学校での推測と証明の通常の実践との間の不協和音は、教育環境でのそのようなツールの広範な使用に対する主要な障壁です。
幾何学自動定理証明器の初期の実装以来、人工知能手法の適用、推論規則に基づく合成証明器、および順連鎖推論の使用は、教育提案により適していると考えられています。
適切なルール セットと、それらのルールを使用できる自動化された方法を選択することは、大きな課題です。
そのようなルール セットの 1 つと、幾何演繹データベース法 (GDDM) を使用したその実装について説明します。
このアプローチは、7 年生のクラス (約 12 歳の学生) の目標となるいくつかの選択された幾何学的な予想を使用してテストされます。
授業計画が提示されます。その目標は、幾何学的定理を証明するための正式なデモンストレーションの導入であり、学生をその目標に向けて動機付けようとします。

要約(オリジナル)

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

arxiv情報

提供元, 利用サービス

arxiv.jp, Google