SP-5

数学証明学習のための原文対論理構造図対応付インタフェース
Web-based Application Assisting Study of Mathematical Proof
with Correspondence between Original Proof and Its Diagram
田中 孝治*1, 宮崎 佳典*2
Koji TANAKA*1, Yoshinori MIYAZAKI*2*1 静岡大学大学院 総合科学技術研究科*1Graduate School of Integrated Science and Technology, Shizuoka University*2 静岡大学学術院 情報学領域*2 College of Informatics, Shizuoka University
Email: tanaka.koji.16@shizuoka.ac.jp
あらまし：本研究では数学証明の学習を促進するための Web アプリケーション開発を行っている．先行研究では，自然言語で記述された数学証明原文の論理構造をフローチャート様の論理構造図で表現するための規則及び作図ツールが開発された．今回は，論理構造図による理解を原文による理解へ転移させることを志向し，原文と論理構造図で表現した証明に含まれる各命題同士を対応付けて提示するためのインタフェースを開発，効果を検証する．
キーワード：e-ラーニング，数学教育，論理構造，GUI アプリケーション

1.

はじめに学校数学における証明の学習に困難を抱える学習者は多い．平成 30 年度の全国学力・学習状況調査
報告書(1)では，問題の条件を変更・追加した時に証明の過程や結果がどう変化するのかを正しく理解し，記述する能力の必要性について触れられている．これに対し，先行研究では証明の過程，すなわち論理構造への理解を補助するために，自然言語で記述された証明の論理構造を図式化する体系が提案され (2)，その有用性が実験によって確認された．
本研究では(2)の体系に従って証明を図式化し，提示するための Web アプリケーション開発を進めている．(3)では教員が GUI 上で教材作成を行うためのオーサリングツールが開発され，実験によりその利便性が確認された．本発表では，証明を図式化したもの（以下，論理構造図とする）による理解を自然言語で記述された証明（以下，原文とする）による理解へ転移させることを志向した機能開発を行う．
そこで，今回は Google 翻訳(4)のインタフェースや，川村(5)の辞書ツールに見られるような原文と翻訳・解説を単語や小節の単位で対比できる機能を参考に，論理構造図と原文を並べて提示し，内包される命題同士の対応関係を明示するための機能及び学習者向けビューワー用のインタフェースを開発する．さらに，その効果を検証するための実験も実施する．

2.

証明図式化体系の概要

ここでは，(2)による証明図式化体系について説明する．体系において，証明中の各命題は矩形に囲まれて示され，証明の構造は矩形同士を線分で結び，上から下への命題の列を作ることで表現する．線分は推論を意味し，線分にラベル付けを行うことで，推論の根拠を記述することができる．ある命題のすぐ上に結ばれている命題を前提，すぐ下に結ばれている命題を帰結と呼ぶ．
この体系では前提となる命題群がすべて真である
ときに，帰結となる命題が真となる関係にある．これにより，複数の前提から１つの帰結を導く構造や，1 つの前提から複数の帰結を導く構造を表現する．
この体系に従って，「自然数𝑎, 𝑏, 𝑐がすべて奇数であるとき，𝑎2 + 𝑏 2 = 𝑐 2 は成り立たない」という証明を図式化すると図 1 のようになる．図中の点線で囲んだ部分は推論根拠をラベル付けしたものである．

図 1 図式化した証明の例

3.

原文対論理構造図対応付インタフェース

今回開発した，原文と論理構造図を並べて提示し，含まれる命題同士の対応関係を明示する機能およびインタフェースについて本節で説明する．この「対応関係の明示」とは，原文と論理構造図の双方に共通して存在する命題について，一方を指定することで，もう一方もハイライトすることを意味する．
3.1 対応付け表示機能
学習者が提示された原文と論理構造図の各命題が持つ対応関係を明示的に参照するための機能について説明する．図 2 は図 1 の論理構造図とその原文と― 301 ―教育システム情報学会 JSiSE2019
第44回全国大会 2019/9/11-9/13が並べて提示されている画面である．左ペインが原文を提示する原文エリア，右ペインが論理構造図を提示する論理構造図エリアである．同画面上にて対応付けされている命題にマウスオーバーすると，図2 中の命題「𝑎2 + 𝑏 2 は偶数」のように，原文と論理構造図の当該命題がオレンジ色にハイライトされる．

クリックすることによって，それらを切り替えることができる．全体ビュー上には，メインビュー上での表示範囲を表す赤枠が存在しており，赤枠をドラッグ＆ドロップで移動させることにより，メインビュー上での表示範囲の変更が可能である．

4.

図 2 原文と論理構造図の提示画面
3.2 対応付け設定機能
ここでは，教員が教材作成を行う段階において，原文と論理構造図を対応付けるための機能について説明する．対応付けは図 3 に示すような手順によって，原文から論理構造図に向けて命題ごとに行う．
まず，原文エリアの原文に対し矩形選択を行う（図3 の①）．続いて選択した箇所をドラッグし，論理構造図エリア上にドロップする（図 3 の②）ことで，対応付けされた命題矩形が作成される（図 3 の③）．

図 3 原文との対応関係を持つ命題の作成手順

実験

開発した原文と論理構造図の対応付け表示機能によって，学習者がその対応関係を意識，活用した学習ができるかを検証するために比較実験を実施する．
実験では，原文対論理構造図対応付インタフェースをもつビューワーに対し，図中のすべての命題が原文上のどこかと対応付けられている論理構造図を提示した状態で，証明の論理構造に関する問題へ解答させる．
某大学の 1 年次用数学基礎科目（2019 年度）を履修する学生を A, B 群に二分し，実験冒頭で(2)の体系およびビューワーについて説明し，例題を用いて解答手順および操作方法の確認を行ったのち，問題 1,2 の順で解答させる．各群とも，うち 1 問は対応付け表示機能を使用可能（そしてもう 1 問は不可能）とし，その設定をクロスさせることで問題間の難易度の差などを吸収させるよう努めている．
両問題とも，ある命題の前提などを問う多肢選択問題と原文上に記述された「与式」などの内容を命題群から選択する問題を出題する．本実験は実験協力者各人の PC および Web ブラウザを用いて行い，解答内容，解答時間及び，命題へのマウスオーバーなど，解答中のアプリケーション使用ログを収集するとともに，事後アンケートを行う．本実験の結果ならびに分析については，発表当日に詳述する．

5.

まとめ

本稿では，(3)で開発された数学証明学習支援のためのアプリケーションに対し，学習者へ向けて新たに追加した原文対論理構造図対応付け機能およびインタフェースについて述べた．今後は，実験で得られた意見等をもとにユーザビリティの改善を行うとともに，論理構造図自体を用いた論理構造への理解や，それを原文へ転移させることをより一層支援する方法について検討してゆく所存である．

3.3 学習者向けインタフェース

参考文献

図 4 論理構造図表示用インタフェース
3.1 節で示した機能を利用した学習を促すために開発したインタフェースについて説明する．論理構
造図エリアの表示には，論理構造図の一部分を大きく表示する「メインビュー」(図 4 右図)と論理構造図全体を一画面に収める「全体ビュー」(図 4 左図)の 2 種類が存在し，論理構造図エリア上部のタブを(1) 国立教育政策研究所:“平成 30 年度 全国学力・学習状況調査 報告書 【中学校／数学】”,（2018）(2) 渡部孝幸, 宮崎佳典, 林佳樹: “導出規則に着目した証明視覚化・式変形支援システムの提案”, 京都大学
数理解析研究所講究録, 第 1865 巻, pp.137-145（2013）(3) 田中孝治, 宮崎佳典: “数学教育における証明学習のための論理構造図式化 GUI アプリケーション”, 日本
e-Learning 学会誌, 第 18 号, pp.7-18（2018）(4) Google: “google 翻訳”, https://translate.google.co.jp/(5) 川村よし子: “初級中級日本語学習者用の辞書ツールの開発”, 第 7 回ヨーロッパ日本語教育シンポジウム（2002）― 302 ―