(57)【要約】【課題】証明問題の学習効果を高める。【解決手段】関数電卓１は、表示部１５と、数学の定理を記憶する定理データベース１３１と、ユーザ操作に基づいて、仮定式及び結論式を含む証明問題を入力する入力部１４と、仮定式から導出される式を定理データベース１３１から読み出して成立式群とするＣＰＵ１１とを備える。入力部１４は、ユーザ操作に基づいて証明問題の解答を１つの式ずつ入力する。ＣＰＵ１１は、入力された入力式が成立式群に含まれるか否かを判定し、含まれると判定された場合にのみ当該入力式を証明問題の解答として表示部１５に表示させる。【選択図】図５
2012137718.tif 000002
【特許請求の範囲】
【請求項１】
表示手段と、
数学の定理を記憶する定理記憶手段と、
ユーザ操作に基づいて、仮定式及び結論式を含む証明問題を入力する証明問題入力手段と、
前記仮定式から導出される式を前記定理記憶手段から読み出して成立式群とする成立式群作成手段と、
ユーザ操作に基づいて前記証明問題の解答を１つの式ずつ入力する解答入力手段と、
前記解答入力手段により入力された入力式が前記成立式群に含まれるか否かを判定する式成立判定手段と、
前記式成立判定手段により前記入力式が前記成立式群に含まれると判定された場合にのみ当該入力式を前記証明問題の解答として前記表示手段に表示させる解答表示手段と、
を備えることを特徴とする計算装置。
【請求項２】
請求項１記載の計算装置において、
前記証明問題は、図形についての問題であり、
当該計算装置は、
ユーザ操作に基づいて前記図形に対する補助線を入力するか、或いは当該補助線の定義を入力する補助線入力手段と、
前記仮定式と、前記補助線を含んだ前記図形の内容とから導出される式を、前記定理記憶手段から読み出して成立式群に追加する成立式群更新手段と、
を備えることを特徴とする計算装置。
【請求項３】
請求項１または２に記載の計算装置において、
前記成立式群作成手段は、
前記仮定式から前記結論式を直接導出する式を前記成立式群から除外する直接導出式除外手段を有することを特徴とする計算装置。
【請求項４】
請求項１〜３の何れか一項に記載の計算装置において、
前記証明問題の解答に不可欠な式を証明不可欠式群として記憶する証明不可欠式群記憶手段と、
前記解答入力手段により入力された入力式が前記証明不可欠式群に含まれるか否かを判定する不可欠式判定手段と、
を備え、
前記解答表示手段は、前記不可欠式判定手段により前記入力式が前記証明不可欠式群に含まれると判定された場合にのみ当該入力式を前記証明問題の解答として前記表示手段に表示させることを特徴とする計算装置。
【請求項５】
表示手段と、
数学の定理を記憶する定理記憶手段と、
ユーザ操作に基づいて、仮定式及び結論式を含む証明問題と、当該証明問題についてユーザが作成した解答とを入力する証明問題・解答入力手段と、
前記仮定式から導出される式を前記定理記憶手段から読み出して成立式群とする成立式群作成手段と、
前記証明問題・解答入力手段により入力された解答中の各式が前記成立式群に含まれるか否かを判定する式成立判定手段と、
前記式成立判定手段により解答中の式が前記成立式群に含まれないと判定される毎に所定の点数から減点した点数を当該解答の評価点とする採点手段と、
を備えることを特徴とする計算装置。
【請求項６】
請求項５記載の計算装置において、
前記証明問題は、図形についての問題であり、
前記証明問題・解答入力手段により入力される解答には、前記図形に対する補助線の定義が含まれ、
当該計算装置は、
前記仮定式と、前記補助線を含んだ前記図形の内容とから導出される式を、前記定理記憶手段から読み出して成立式群に追加する成立式群更新手段と、
を備えることを特徴とする計算装置。
【請求項７】
請求項５または６に記載の計算装置において、
前記成立式群作成手段は、
前記仮定式から前記結論式を直接導出する式を前記成立式群から除外する直接導出式除外手段を有することを特徴とする計算装置。
【請求項８】
請求項５〜７の何れか一項に記載の計算装置において、
前記証明問題の解答に不可欠な式を証明不可欠式群として記憶する証明不可欠式群記憶手段と、
前記証明問題・解答入力手段により入力された解答中の各式が前記証明不可欠式群に含まれるか否かを判定する不可欠式判定手段と、
を備え、
前記採点手段は、
前記不可欠式判定手段により解答中の式が前記証明不可欠式群に含まれないと判定される毎に所定の点数から減点した点数を当該解答の評価点とすることを特徴とする計算装置。
【請求項９】
表示手段を有するコンピュータに、
数学の定理を記憶する定理記憶機能と、
ユーザ操作に基づいて、仮定式及び結論式を含む証明問題を入力する証明問題入力機能と、
前記仮定式から導出される式を前記定理記憶機能による記憶内容から読み出して成立式群とする成立式群作成機能と、
ユーザ操作に基づいて前記証明問題の解答を１つの式ずつ入力する解答入力機能と、
前記解答入力機能により入力された入力式が前記成立式群に含まれるか否かを判定する式成立判定機能と、
前記式成立判定機能により前記入力式が前記成立式群に含まれると判定された場合にのみ当該入力式を前記証明問題の解答として前記表示手段に表示させる解答表示機能と、
を実現させることを特徴とするプログラム。
【請求項１０】
表示手段を有するコンピュータに、
数学の定理を記憶する定理記憶機能と、
ユーザ操作に基づいて、仮定式及び結論式を含む証明問題と、当該証明問題についてユーザが作成した解答とを入力する証明問題・解答入力機能と、
前記仮定式から導出される式を前記定理記憶機能による記憶内容から読み出して成立式群とする成立式群作成機能と、
前記証明問題・解答入力機能により入力された解答中の各式が前記成立式群に含まれるか否かを判定する式成立判定機能と、
前記式成立判定機能により解答中の式が前記成立式群に含まれないと判定される毎に所定の点数から減点した点数を当該解答の評価点とする採点機能と、
を実現させることを特徴とするプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、計算装置及びプログラムに関する。
【背景技術】
【０００２】
従来、関数電卓などの計算装置においては、幾何学の学習を補助する技術が提案されている（例えば、特許文献１参照）。具体的には、この特許文献１の技術においては、図形問題の図中に補助線を描画することで、学習効果を高めるようになっている。
【先行技術文献】
【特許文献】
【０００３】
【特許文献１】特開２００９−９０５９号公報
【発明の概要】
【発明が解決しようとする課題】
【０００４】
しかしながら、従来の技術では、証明問題の学習効果を高めることはできない。具体的には、証明問題において、入力される解答が誤っている場合としては、論理的には合っていても証明に必要ではない内容を解答が含んでいる場合や、論理的に誤った内容を解答が含んでいる場合があるところ、従来の技術ではこのような誤解答を検出することはできない。
【０００５】
本発明の課題は、証明問題の学習効果を高めることのできる計算装置及びプログラムを提供することである。
【課題を解決するための手段】
【０００６】
以上の課題を解決するため、請求項１に記載の発明は、計算装置において、
表示手段と、
数学の定理を記憶する定理記憶手段と、
ユーザ操作に基づいて、仮定式及び結論式を含む証明問題を入力する証明問題入力手段と、
前記仮定式から導出される式を前記定理記憶手段から読み出して成立式群とする成立式群作成手段と、
ユーザ操作に基づいて前記証明問題の解答を１つの式ずつ入力する解答入力手段と、
前記解答入力手段により入力された入力式が前記成立式群に含まれるか否かを判定する式成立判定手段と、
前記式成立判定手段により前記入力式が前記成立式群に含まれると判定された場合にのみ当該入力式を前記証明問題の解答として前記表示手段に表示させる解答表示手段と、
を備えることを特徴とする。
【０００７】
請求項２記載の発明は、請求項１記載の計算装置において、
前記証明問題は、図形についての問題であり、
当該計算装置は、
ユーザ操作に基づいて前記図形に対する補助線を入力するか、或いは当該補助線の定義を入力する補助線入力手段と、
前記仮定式と、前記補助線を含んだ前記図形の内容とから導出される式を、前記定理記憶手段から読み出して成立式群に追加する成立式群更新手段と、
を備えることを特徴とする。
【０００８】
請求項３記載の発明は、請求項１または２に記載の計算装置において、
前記成立式群作成手段は、
前記仮定式から前記結論式を直接導出する式を前記成立式群から除外する直接導出式除外手段を有することを特徴とする。
【０００９】
請求項４記載の発明は、請求項１〜３の何れか一項に記載の計算装置において、
前記証明問題の解答に不可欠な式を証明不可欠式群として記憶する証明不可欠式群記憶手段と、
前記解答入力手段により入力された入力式が前記証明不可欠式群に含まれるか否かを判定する不可欠式判定手段と、
を備え、
前記解答表示手段は、前記不可欠式判定手段により前記入力式が前記証明不可欠式群に含まれると判定された場合にのみ当該入力式を前記証明問題の解答として前記表示手段に表示させることを特徴とする。
【００１０】
請求項５記載の発明は、計算装置において、
表示手段と、
数学の定理を記憶する定理記憶手段と、
ユーザ操作に基づいて、仮定式及び結論式を含む証明問題と、当該証明問題についてユーザが作成した解答とを入力する証明問題・解答入力手段と、
前記仮定式から導出される式を前記定理記憶手段から読み出して成立式群とする成立式群作成手段と、
前記証明問題・解答入力手段により入力された解答中の各式が前記成立式群に含まれるか否かを判定する式成立判定手段と、
前記式成立判定手段により解答中の式が前記成立式群に含まれないと判定される毎に所定の点数から減点した点数を当該解答の評価点とする採点手段と、
を備えることを特徴とする。
【００１１】
請求項６記載の発明は、請求項５記載の計算装置において、
前記証明問題は、図形についての問題であり、
前記証明問題・解答入力手段により入力される解答には、前記図形に対する補助線の定義が含まれ、
当該計算装置は、
前記仮定式と、前記補助線を含んだ前記図形の内容とから導出される式を、前記定理記憶手段から読み出して成立式群に追加する成立式群更新手段と、
を備えることを特徴とする。
【００１２】
請求項７記載の発明は、請求項５または６に記載の計算装置において、
前記成立式群作成手段は、
前記仮定式から前記結論式を直接導出する式を前記成立式群から除外する直接導出式除外手段を有することを特徴とする。
【００１３】
請求項８記載の発明は、請求項５〜７の何れか一項に記載の計算装置において、
前記証明問題の解答に不可欠な式を証明不可欠式群として記憶する証明不可欠式群記憶手段と、
前記証明問題・解答入力手段により入力された解答中の各式が前記証明不可欠式群に含まれるか否かを判定する不可欠式判定手段と、
を備え、
前記採点手段は、
前記不可欠式判定手段により解答中の式が前記証明不可欠式群に含まれないと判定される毎に所定の点数から減点した点数を当該解答の評価点とすることを特徴とする。
【００１４】
請求項９記載の発明は、プログラムにおいて、
表示手段を有するコンピュータに、
数学の定理を記憶する定理記憶機能と、
ユーザ操作に基づいて、仮定式及び結論式を含む証明問題を入力する証明問題入力機能と、
前記仮定式から導出される式を前記定理記憶機能による記憶内容から読み出して成立式群とする成立式群作成機能と、
ユーザ操作に基づいて前記証明問題の解答を１つの式ずつ入力する解答入力機能と、
前記解答入力機能により入力された入力式が前記成立式群に含まれるか否かを判定する式成立判定機能と、
前記式成立判定機能により前記入力式が前記成立式群に含まれると判定された場合にのみ当該入力式を前記証明問題の解答として前記表示手段に表示させる解答表示機能と、
を実現させることを特徴とする。
【００１５】
請求項１０記載の発明は、プログラムにおいて、
表示手段を有するコンピュータに、
数学の定理を記憶する定理記憶機能と、
ユーザ操作に基づいて、仮定式及び結論式を含む証明問題と、当該証明問題についてユーザが作成した解答とを入力する証明問題・解答入力機能と、
前記仮定式から導出される式を前記定理記憶機能による記憶内容から読み出して成立式群とする成立式群作成機能と、
前記証明問題・解答入力機能により入力された解答中の各式が前記成立式群に含まれるか否かを判定する式成立判定機能と、
前記式成立判定機能により解答中の式が前記成立式群に含まれないと判定される毎に所定の点数から減点した点数を当該解答の評価点とする採点機能と、
を実現させることを特徴とする。
【発明の効果】
【００１６】
本発明の第１の側面によれば、仮定式及び結論式を含む証明問題が入力されると、仮定式から導出される式が読み出されて成立式群とされ、ユーザ操作に基づいて証明問題の解答が１つの式ずつ入力されると、入力式が成立式群に含まれる場合にのみ当該入力式が証明問題の解答として表示されるので、論理的に誤った内容が解答に含まれるのを防止することができる。従って、証明問題の学習効果を高めることができる。
【００１７】
また、本発明の第２の側面によれば、仮定式及び結論式を含む証明問題と、当該証明問題についてユーザが作成した解答とが入力されると、仮定式から導出される式が読み出されて成立式群とされて、解答中の各式が成立式群に含まれるか否かが判定され、含まれないと判定される毎に所定の点数から減点した点数が当該解答の評価点とされるので、論理的に誤った内容を解答内から検出して採点することができる。従って、証明問題の学習効果を高めることができる。
【図面の簡単な説明】
【００１８】
【図１】関数電卓の概略構成を示す平面図である。
【図２】関数電卓の機能構成を示すブロック図である。
【図３】定理データベースのデータ構造を示す図である。
【図４】情報表示処理の流れを示すフローチャートである。
【図５】ディスプレイの表示内容を示す図である。
【図６】ディスプレイの表示内容を示す図である。
【図７】第２実施形態における情報表示処理の流れを示すフローチャートである。
【発明を実施するための最良の形態】
【００１９】
以下、添付図面を参照して本発明に係る実施の形態の一例を詳細に説明する。ただし、発明の範囲は、図示例に限定されない。
【００２０】
＜第１の実施形態＞
［１．１  外観構成］
図１は、本発明に係る計算装置を適用した関数電卓１の概略構成を示す平面図である。
この図に示すように、関数電卓１は、各種キー群を有する入力キー群２と、ディスプレイ３と、を備えている。
【００２１】
入力キー群２は、ユーザから数値や演算記号等の数式構成要素の入力操作を受けたり、各種処理の指示操作を受けたりするためのキー群であり、それぞれ固有の機能を割り当てられた複数のキーを備えている。本実施の形態においては、入力キー群２は、テンキー２０や演算記号キー２１、カーソルキー２２、ＥＸＥキー２３、削除キー２４等を備えている。
【００２２】
このうち、テンキー２０は数値の入力操作を受けるキーであり、演算記号キー２１は四則演算の記号や括弧、分数の括線、根号（√）、対数記号、定数（円周率「π」や光速度「ｃ」等）、三角関数記号など、各種演算記号の入力操作を受けるキーである。
【００２３】
カーソルキー２２は、ディスプレイ３内で編集対象位置や選択対象位置を示すカーソルを所定の方向に移動させる場合等に押下されるキーであり、本実施の形態においては、上下左右の４方向について入力可能に構成されている。
【００２４】
ＥＸＥキー２３は、処理の実行指示や決定指示の入力操作を受けるキーであり、例えば数式の入力後に演算処理の実行を指示するキーとして機能するようになっている。削除キー２４は、ディスプレイ３に表示されている数値や演算記号などの削除操作を受けるキーである。
【００２５】
ディスプレイ３は、ＬＣＤ（Liquid Crystal Display）やＥＬＤ（Electronic Luminescent Display）等により構成されており、入力キー群２などの操作に応じた文字や符号、数式、演算結果などの他、関数電卓１を使用するために必要な各種データを表示するようになっている。なお、本実施の形態におけるディスプレイ３には、タッチパネル３０が表示画面全面に亘って一体的に設けられている。
【００２６】
［１．２  機能構成］
続いて、関数電卓１の機能構成を説明する。
図２は、関数電卓１の概略的な機能構成を示すブロック図である。
【００２７】
この図に示すように、関数電卓１は、入力部１４と、表示部１５と、インターフェース１６と、記憶部１３と、ＲＡＭ（Random Access Memory）１２と、ＣＰＵ（Central Processing Unit）１１と、を備えて構成されている。
【００２８】
入力部１４は、上述の入力キー群２及びタッチパネル３０を備えており、押下されたキーやタッチパネル３０の位置に対応する信号をＣＰＵ１１に出力するようになっている。
【００２９】
表示部１５は、上述のディスプレイ３を備えており、ＣＰＵ１１からの表示信号に従って各種情報をディスプレイ３に表示するようになっている。
【００３０】
インターフェース１６は、図示しない外部機器に接続するための接続端子であり、本実施の形態においては、ＵＳＢケーブルなどを介して外部機器から後述の画像ファイル１３２などを読み込んで、記憶部１３に記憶させることができるようになっている。なお、このインターフェース１６は、カード媒体などの記録媒体からデータを読み込むこととしても良い。
【００３１】
記憶部１３は、ＲＯＭ（Read  Only  Memory）等により構成される不揮発性のメモリであり、各種プログラム及び各種データを記憶している。具体的には、記憶部１３は、本発明に係るプログラムとしての情報表示プログラム１３０と、定理データベース１３１と、証明不可欠式群テーブル１３２等とを記憶している。
【００３２】
情報表示プログラム１３０は、後述の情報表示処理（図４参照）をＣＰＵ１１に実行させるためのプログラムである。
【００３３】
定理データベース１３１は、数学の定理を記憶するものであり、例えば図３に示すように、図形内で満たされる条件と、当該条件下で成立する結論式とを対応付けて複数記憶している。
【００３４】
証明不可欠式群テーブル１３２は、仮定式と結論式とを含む証明問題の解答に不可欠な１以上の式（以下、証明不可欠式群とする）を記憶するものであり、証明問題と、その証明不可欠式群とを対応付けて複数記憶している。なお、この証明不可欠式群テーブル１３２内の情報は、ユーザが入力することとしてもよいし、インターフェース１６等を介して外部機器から取得されることとしてもよい。
【００３５】
ＲＡＭ１２は、情報を一時的に格納する揮発性のメモリであり、実行される各種プログラムやこれら各種プログラムに係るデータ等を格納する複数のワークエリアを有する。具体的には、本実施の形態におけるＲＡＭ１２は、成立式群記憶領域１２０や証明不可欠式群記憶領域１２１等を有している。
【００３６】
成立式群記憶領域１２０には、後述の情報表示処理（図４参照）において証明問題の仮定式から導出される１以上の式が成立式群として記憶されるようになっている。
【００３７】
証明不可欠式群記憶領域１２１には、後述の情報表示処理（図４参照）において証明問題に対応する証明不可欠式群が記憶されるようになっている。
【００３８】
ＣＰＵ１１は、関数電卓１の各部を中央制御する。具体的には、ＣＰＵ１１は、記憶部１３に記憶されているシステムプログラム及び各種アプリケーションプログラムの中から指定されたプログラムをＲＡＭ１２に展開し、ＲＡＭ１２に展開されたプログラムとの協働で、各種処理を実行する。
【００３９】
［１．３  関数電卓の動作］
続いて、関数電卓１の動作について説明する。
【００４０】
図４は、情報表示処理の動作を説明するためのフローチャートである。なお、この情報表示処理は、ユーザにより入力部１４を介して情報表示処理の実行指示が入力されると、記憶部１３から情報表示プログラム１３０が読み出されてＲＡＭ１２に適宜展開される結果、当該情報表示プログラム１３０とＣＰＵ１１との協働によって実行される。
【００４１】
この図に示すように、情報表示処理においては、まずユーザが証明問題における仮定式及び結論式を入力すると、ＣＰＵ１１は、入力内容をディスプレイ３に表示させる（ステップＳ１）。ここで、本実施の形態においては、この証明問題は図形についての問題となっており、このステップＳ１においてユーザは、当該証明問題についての図形も入力してディスプレイ３に表示させることとして説明する。また、本実施の形態においては、証明問題の証明不可欠式群が当該証明問題に対応付けられて予め記憶されているが、このステップＳ１においてユーザが証明不可欠式群を入力することとしても良い。
【００４２】
次に、ＣＰＵ１１は、仮定式及び図形から導出される式を成立式群として定理データベース１３１から読み出し、成立式群記憶領域１２０に記憶させる（ステップＳ２）。また、このときＣＰＵ１１は、証明不可欠式群テーブル１３２から証明問題に対応する証明不可欠式群を読み出して、証明不可欠式群記憶領域１２１に記憶させる。但し、ステップＳ１において証明不可欠式群がユーザから入力された場合には、ＣＰＵ１１は、その入力式を証明不可欠式群記憶領域１２１に記憶させる。
【００４３】
次に、ＣＰＵ１１は、仮定式から結論式を直接導く式、すなわち一つの式で仮定式から結論式が導かれることが自明な式が成立式群中に含まれるか否かを判定し（ステップＳ３）、含まれないと判定した場合（ステップＳ３；Ｎｏ）には、後述のステップＳ５に移行する。
【００４４】
また、ステップＳ３において仮定式から結論式を直接導く式が成立式群中に含まれると判定した場合（ステップＳ３；Ｙｅｓ）には、ＣＰＵ１１は、その式を成立式群記憶領域１２０から削除する（ステップＳ４）。
【００４５】
次に、ＣＰＵ１１は、ディスプレイ３に表示されている図形に対して補助線が引かれるか否かを判定し（ステップＳ５）、引かれないと判定した場合（ステップＳ５；Ｎｏ）には、後述のステップＳ６に移行する。
【００４６】
また、ステップＳ５において補助線が引かれたと判定した場合（ステップＳ５；Ｙｅｓ）には、ＣＰＵ１１は、この補助線を含めた図形の内容と、仮定式とから新たに導出される式を成立式として定理データベース１３１から読み出し、成立式群記憶領域１２０に追加記憶させる（ステップＳ６）。
【００４７】
次に、ＣＰＵ１１は、解答の式が１つ入力されたか否かを判定し（ステップＳ７）、入力されないと判定した場合（ステップＳ７；Ｎｏ）、つまり式以外の内容（補助線の定義など）が入力されたと判定した場合には、その入力内容をディスプレイ３に表示させた後（ステップＳ８）、後述のステップＳ１４に移行する。
【００４８】
また、ステップＳ７において解答の式が１つ入力されたと判定した場合（ステップＳ７；Ｙｅｓ）には、ＣＰＵ１１は、入力式が成立式群記憶領域１２０における何れかの式と合致するか否か、つまり成立式群に含まれるか否かを判定する（ステップＳ９）。
【００４９】
このステップＳ９において入力式が成立式群に含まれないと判定した場合（ステップＳ９；Ｎｏ）には、ＣＰＵ１１は、入力式が誤った内容である旨をディスプレイ３に表示させた後（ステップＳ１０）、後述のステップＳ１４に移行する。
【００５０】
また、ステップＳ９において入力式が成立式群に含まれると判定した場合（ステップＳ９；Ｙｅｓ）には、ＣＰＵ１１は、入力式が証明不可欠式群記憶領域１２１における何れかの式と合致するか否か、つまり証明不可欠式群に含まれるか否かを判定する（ステップＳ１１）。
【００５１】
このステップＳ１１において入力式が証明不可欠式群に含まれないと判定した場合（ステップＳ１１；Ｎｏ）には、ＣＰＵ１１は、入力式が証明に不要な内容である旨をディスプレイ３に表示させた後（ステップＳ１２）、後述のステップＳ１４に移行する。
【００５２】
また、ステップＳ１１において入力式が証明不可欠式群に含まれると判定した場合（ステップＳ１１；Ｙｅｓ）には、ＣＰＵ１１は、入力式を証明問題の解答としてディスプレイ３に表示させた後（ステップＳ１３）、解答の入力を終了する旨の操作が行われるか否かを判定する（ステップＳ１４）。
【００５３】
このステップＳ１４において解答の入力を終了する旨の操作が行われないと判定した場合（ステップＳ１４；Ｎｏ）には、ＣＰＵ１１は、上述のステップＳ５に移行する。
【００５４】
また、ステップＳ１４において解答の入力を終了する旨の操作が行われたと判定した場合（ステップＳ１４；Ｙｅｓ）には、ＣＰＵ１１は、証明不可欠式群記憶領域１２１に記憶された各式と、入力式とを比較して、証明不可欠式群が全て入力されているか否かを判定する（ステップＳ１５）。
【００５５】
このステップＳ１５において証明不可欠式群が全ては入力されていないと判定した場合（ステップＳ１５；Ｎｏ）には、ＣＰＵ１１は、入力すべき式が未だ残っている旨をディスプレイ３に表示させた後（ステップＳ１６）、上述のステップＳ５に移行する。
【００５６】
また、ステップＳ１５において証明不可欠式群が全て入力されたと判定した場合（ステップＳ１５；Ｙｅｓ）には、ＣＰＵ１１は、情報表示処理を終了する。
【００５７】
［１．４  動作例］
続いて、図面を参照しつつ、上述した関数電卓１の動作を具体的に説明する。
【００５８】
まず、ユーザが証明問題における仮定式「ＡＢ＝ＡＣ」及び結論式「∠ＡＢＣ＝∠ＡＣＢ」と、２等辺３角形「ＡＢＣ」とを入力すると、図５（ａ）に示すように、入力内容がディスプレイ３に表示される（ステップＳ１）。
【００５９】
次に、図３に示すように、仮定式「ＡＢ＝ＡＣ」及び図形から導出される式「ＡＢ＝ＡＣ」，「∠ＡＢＣ＝∠ＡＣＢ」が成立式群として定理データベース１３１から読み出され、成立式群記憶領域１２０に記憶される（ステップＳ２）。また、このとき証明不可欠式群テーブル１３２から証明問題に対応する証明不可欠式群が読み出されて、証明不可欠式群記憶領域１２１に記憶される。
【００６０】
次に、仮定式「ＡＢ＝ＡＣ」から結論式「∠ＡＢＣ＝∠ＡＣＢ」を直接導く式「∠ＡＢＣ＝∠ＡＣＢ」が成立式群中に含まれると判定され（ステップＳ３；Ｙｅｓ）、その式「∠ＡＢＣ＝∠ＡＣＢ」が成立式群記憶領域１２０から削除される（ステップＳ４）。
【００６１】
次に、図５（ｂ）に示すように、ユーザが∠ＢＡＣの２等分線として補助線ＡＤを引くと（ステップＳ５；Ｙｅｓ）、図３に示すように、この補助線ＡＤを含めた図形の内容と、仮定式「ＡＢ＝ＡＣ」とから新たに導出される式「△ＡＢＤ≡△ＡＣＤ」，「ＡＢ＝ＡＣ」，「ＡＤ＝ＡＤ」，「ＢＤ＝ＣＤ」，「∠ＢＡＤ＝∠ＣＡＤ」，…が成立式として定理データベース１３１から読み出され、成立式群記憶領域１２０に追加記憶される（ステップＳ６）。
【００６２】
次に、ユーザが補助線の定義「∠ＢＡＣの二等分線を引き、ＢＣとの交点をＤとする」を入力すると（ステップＳ７；Ｎｏ）、その入力内容がディスプレイ３に表示される（ステップＳ８）。
【００６３】
次に、図５（ｃ）に示すように、ユーザが解答の式「ＡＢ＝ＡＣ」を入力すると（ステップＳ７；Ｙｅｓ）、入力式「ＡＢ＝ＡＣ」が成立式群記憶領域１２０における式「ＡＢ＝ＡＣ」と合致し（ステップＳ９；Ｙｅｓ）、かつ、証明不可欠式群記憶領域１２１における式「ＡＢ＝ＡＣ」と合致する（ステップＳ１１；Ｙｅｓ）と判定され、入力式「ＡＢ＝ＡＣ」が証明問題の解答としてディスプレイ３に表示される（ステップＳ１３）。
【００６４】
次に、図５（ｄ）に示すように、ユーザが解答の式「∠ＢＡＤ＝∠ＣＡＤ」を入力すると（ステップＳ７；Ｙｅｓ）、入力式「∠ＢＡＤ＝∠ＣＡＤ」が成立式群記憶領域１２０における式「∠ＢＡＤ＝∠ＣＡＤ」と合致し（ステップＳ９；Ｙｅｓ）、かつ、証明不可欠式群記憶領域１２１における式「∠ＢＡＤ＝∠ＣＡＤ」と合致する（ステップＳ１１；Ｙｅｓ）と判定され、入力式「∠ＢＡＤ＝∠ＣＡＤ」が証明問題の解答としてディスプレイ３に表示される（ステップＳ１３）。
【００６５】
次に、図６（ａ）に示すように、ユーザが解答の式「ＢＤ＝ＣＤ」を入力すると（ステップＳ７；Ｙｅｓ）、入力式「ＢＤ＝ＣＤ」が成立式群記憶領域１２０における式「ＢＤ＝ＣＤ」と合致し（ステップＳ９；Ｙｅｓ）、かつ、証明不可欠式群に含まれない（ステップＳ１１；Ｎｏ）と判定され、入力式「ＢＤ＝ＣＤ」が証明に不要な内容である旨がディスプレイ３に表示される（ステップＳ１２）。
【００６６】
次に、図６（ｂ）に示すように、ユーザが解答の式「△ＡＢＤ≡△ＡＣＤ」を入力すると（ステップＳ７；Ｙｅｓ）、入力式「△ＡＢＤ≡△ＡＣＤ」が成立式群記憶領域１２０における式「△ＡＢＤ≡△ＡＣＤ」と合致し（ステップＳ９；Ｙｅｓ）、かつ、証明不可欠式群記憶領域１２１における式「△ＡＢＤ≡△ＡＣＤ」と合致する（ステップＳ１１；Ｙｅｓ）と判定され、入力式「△ＡＢＤ≡△ＡＣＤ」が証明問題の解答としてディスプレイ３に表示される（ステップＳ１３）。
【００６７】
次に、図６（ｃ）に示すように、ユーザが解答の式「ＡＢ＝ＢＣ」を入力すると（ステップＳ７；Ｙｅｓ）、入力式「ＡＢ＝ＢＣ」が成立式群に含まれないと判定され（ステップＳ９；Ｎｏ）、入力式が誤った内容である旨がディスプレイ３に表示される（ステップＳ１０）。
【００６８】
次に、図６（ｄ）に示すように、ユーザが解答の式「∠ＡＢＣ＝∠ＡＣＢ」を入力すると（ステップＳ７；Ｙｅｓ）、入力式「∠ＡＢＣ＝∠ＡＣＢ」が成立式群記憶領域１２０における式「∠ＡＢＣ＝∠ＡＣＢ」と合致し（ステップＳ９；Ｙｅｓ）、かつ、証明不可欠式群記憶領域１２１における式「∠ＡＢＣ＝∠ＡＣＢ」と合致する（ステップＳ１１；Ｙｅｓ）と判定され、入力式「∠ＡＢＣ＝∠ＡＣＢ」が証明問題の解答としてディスプレイ３に表示される（ステップＳ１３）。
【００６９】
そして、解答の入力を終了する旨の操作をユーザが行うと（ステップＳ１４；Ｙｅｓ）、証明不可欠式群が全て入力されていると判定され（ステップＳ１５；Ｙｅｓ）、情報表示処理が終了する。
【００７０】
以上、本実施の形態によれば、図４のステップＳ２，Ｓ９や、図５〜図６等に示したように、仮定式及び結論式を含む証明問題が入力されると、仮定式から導出される式が読み出されて成立式群とされ、ユーザ操作に基づいて証明問題の解答が１つの式ずつ入力されると、入力式が成立式群に含まれる場合にのみ当該入力式が証明問題の解答として表示されるので、論理的に誤った内容が解答に含まれるのを防止することができる。従って、証明問題の学習効果を高めることができる。
【００７１】
また、図４のステップＳ１２や図６（ａ）等に示したように、証明問題の解答に不可欠な式が証明不可欠式群として記憶され、入力式が証明不可欠式群に含まれると判定された場合にのみ当該入力式が証明問題の解答として表示されるので、論理的には合っていても証明に必要ではない内容が解答に含まれるのを防止することができる。従って、証明問題の学習効果をいっそう高めることができる。
【００７２】
また、図４のステップＳ３〜Ｓ４等に示したように、仮定式から結論式を直接導出する式が成立式群から除外されるので、一般的にはよく知られている定理であっても、他の定理から順を追った論理的な解答を入力させることができる。従って、初学者に対しても証明問題の学習効果を確実に高めることができる。
【００７３】
＜第２の実施形態＞
続いて、本発明の第２の実施形態について説明する。なお、上記第１の実施形態と同様の構成要素には同一の符号を付し、その説明を省略する。
【００７４】
図２に示すように、本実施形態における関数電卓１Ａの記憶部１３Ａは情報表示プログラム１３０Ａを記憶している。
【００７５】
この情報表示プログラム１３０Ａは、後述の情報表示処理（図７参照）をＣＰＵ１１に実行させるためのプログラムである。
【００７６】
また、関数電卓１ＡのＲＡＭ１２Ａは、評価点記憶領域１２２を有している。
この評価点記憶領域１２２には、後述の情報表示処理（図７参照）において証明問題の解答の評価点が記憶されるようになっている。
【００７７】
続いて、関数電卓１Ａの動作について説明する。
図７は、情報表示処理の動作を説明するためのフローチャートである。なお、この情報表示処理は、ユーザにより入力部１４を介して情報表示処理の実行指示が入力されると、記憶部１３Ａから情報表示プログラム１３０Ａが読み出されてＲＡＭ１２に適宜展開される結果、当該情報表示プログラム１３０ＡとＣＰＵ１１との協働によって実行される。
【００７８】
この図に示すように、情報表示処理においては、まずユーザが証明問題における仮定式、結論式と、当該証明問題の解答とを入力すると、ＣＰＵ１１は、入力内容をディスプレイ３に表示させるとともに、当該証明問題の配点を評価点記憶領域１２２に記憶させる（ステップＴ１）。ここで、本実施の形態においては、この証明問題は図形についての問題となっており、このステップＴ１においてユーザは、当該証明問題についての図形も入力してディスプレイ３に表示させることとして説明する。また、本実施の形態においては、このとき入力される解答には、図形に対する補助線の定義が含まれていても良い。また、本実施の形態においては、証明問題の証明不可欠式群が当該証明問題に対応付けられて予め記憶されているが、このステップＴ１においてユーザが証明不可欠式群を入力することとしても良い。更に、このステップＴ１において「入力」とは、インターフェース１６を介して外部機器から関数電卓１に入力することを含む。
【００７９】
次に、ＣＰＵ１１は、仮定式及び図形から導出される式を成立式群として定理データベース１３１から読み出し、成立式群記憶領域１２０に記憶させる（ステップＴ２）。また、このときＣＰＵ１１は、証明不可欠式群テーブル１３２から証明問題に対応する証明不可欠式群を読み出して、証明不可欠式群記憶領域１２１に記憶させる。但し、ステップＴ１において証明不可欠式群がユーザから入力された場合には、ＣＰＵ１１は、その入力式を証明不可欠式群記憶領域１２１に記憶させる。
【００８０】
次に、ＣＰＵ１１は、仮定式から結論式を直接導く式が成立式群中に含まれるか否かを判定し（ステップＴ３）、含まれないと判定した場合（ステップＴ３；Ｎｏ）には、後述のステップＴ５に移行する。
【００８１】
また、ステップＴ３において仮定式から結論式を直接導く式が成立式群中に含まれると判定した場合（ステップＴ３；Ｙｅｓ）には、ＣＰＵ１１は、その式を成立式群記憶領域１２０から削除する（ステップＴ４）。
【００８２】
次に、ＣＰＵ１１は、カウント値「ｎ」を「１」とした後（ステップＴ５）、解答における「ｎ」番目の記載項目が図形に対する補助線の定義であるか否かを判定し（ステップＴ６）、補助線の定義ではないと判定した場合（ステップＴ６；Ｎｏ）には、後述のステップＴ８に移行する。
【００８３】
また、ステップＴ６において「ｎ」番目の記載項目が図形に対する補助線の定義であると判定した場合（ステップＴ６；Ｙｅｓ）には、ＣＰＵ１１は、この補助線を含めた図形の内容と、仮定式とから新たに導出される式を成立式として定理データベース１３１から読み出し、成立式群記憶領域１２０に追加記憶させる（ステップＴ７）。
【００８４】
次に、ＣＰＵ１１は、解答における「ｎ」番目の記載項目が式であるか否かを判定し（ステップＴ８）、式でないと判定した場合（ステップＴ８；Ｎｏ）、つまり式以外の内容であると判定した場合には、後述のステップＴ１４に移行する。
【００８５】
また、ステップＴ８において解答における「ｎ」番目の記載項目が式であると判定した場合（ステップＴ８；Ｙｅｓ）には、ＣＰＵ１１は、当該式が成立式群記憶領域１２０における何れかの式と合致するか否か、つまり成立式群に含まれるか否かを判定する（ステップＴ９）。
【００８６】
このステップＴ９において「ｎ」番目の記載項目の式が成立式群に含まれないと判定した場合（ステップＴ９；Ｎｏ）、つまり当該式が誤った内容である場合には、ＣＰＵ１１は、評価点記憶領域１２２に記憶されている点数から３点を引くとともに、３点の減点を行った旨を当該式部分の近傍に表示させた後（ステップＴ１０）、後述のステップＴ１４に移行する。
【００８７】
また、ステップＴ９において「ｎ」番目の記載項目の式が成立式群に含まれると判定した場合（ステップＴ９；Ｙｅｓ）には、ＣＰＵ１１は、当該式が証明不可欠式群記憶領域１２１における何れかの式と合致するか否か、つまり証明不可欠式群に含まれるか否かを判定する（ステップＴ１１）。
【００８８】
このステップＴ１１において「ｎ」番目の記載項目の式が証明不可欠式群に含まれないと判定した場合（ステップＴ１１；Ｎｏ）、つまり当該式が証明に不要な内容である場合には、ＣＰＵ１１は、評価点記憶領域１２２に記憶されている点数から１点を引くとともに、１点の減点を行った旨を当該式部分の近傍に表示させた後（ステップＴ１２）、後述のステップＴ１４に移行する。
【００８９】
また、ステップＴ１１において「ｎ」番目の記載項目の式が証明不可欠式群に含まれると判定した場合（ステップＴ１１；Ｎｏ）には、ＣＰＵ１１は、減点が無い旨を当該式部分の近傍に表示させる（ステップＴ１３）。
【００９０】
次に、ＣＰＵ１１は、「ｎ」番目の記載項目が解答中の最後の項目であるか否かを判定し（ステップＴ１４）、最後ではないと判定した場合（ステップＴ１４；Ｎｏ）には、カウント値「ｎ」に「１」を加えた後（ステップＴ１５）、上述のステップＴ６に移行する。
【００９１】
また、ステップＴ１４において「ｎ」番目の記載項目が解答中の最後の項目であると判定した場合（ステップＴ１４；Ｙｅｓ）には、ＣＰＵ１１は、証明不可欠式群記憶領域１２１に記憶された各式と、解答中の各式とを比較して、解答中に証明不可欠式群が全て含まれるか否かを判定する（ステップＴ１６）。
【００９２】
そして、このステップＴ１６において証明不可欠式群が全ては含まれていないと判定した場合（ステップＴ１６；Ｎｏ）には、ＣＰＵ１１は、不足している式１つにつき５点を、評価点記憶領域１２２に記憶されている点数から引いた後（ステップＴ１７）、評価点記憶領域１２２内の点数を解答の評価点としてディスプレイ３に表示させて情報表示処理を終了する。
【００９３】
また、ステップＴ１６において証明不可欠式群が全て含まれると判定した場合（ステップＴ１６；Ｙｅｓ）には、ＣＰＵ１１は、評価点記憶領域１２２内の点数を解答の評価点としてディスプレイ３に表示させて情報表示処理を終了する。
【００９４】
なお、上記のステップＴ１０、Ｔ１２、１３及びＴ１７における減点数は例示であり、具体的な数値をこれらに限るものではないが、好ましくはステップＴ１０における減点がステップＴ１２における減点よりも大きく、ステップＴ１２における減点がステップＴ１３における減点よりも大きい。また、好ましくはステップＴ１７における減点がステップＴ１３における減点よりも大きい。さらに好ましくは、ステップＴ１７における減点はステップＴ１０における減点よりも大きい。
【００９５】
以上、本実施の形態によれば、図７のステップＴ２，Ｔ９〜Ｔ１０等に示したように、仮定式及び結論式を含む証明問題と、当該証明問題についてユーザが作成した解答とが入力されると、仮定式から導出される式が読み出されて成立式群とされて、解答中の各式が成立式群に含まれるか否かが判定され、含まれないと判定される毎に所定の点数から減点した点数が当該解答の評価点とされるので、論理的に誤った内容を解答内から検出して採点することができる。従って、証明問題の学習効果を高めることができる。
【００９６】
また、図７のステップＴ１１〜Ｔ１２等に示したように、証明問題の解答に不可欠な式が証明不可欠式群として記憶され、入力式が証明不可欠式群に含まれないと判定される毎に所定の点数から減点した点数が当該解答の評価点とされるので、論理的には合っていても証明に必要ではない内容を解答内から検出して採点することができる。従って、証明問題の学習効果をいっそう高めることができる。
【００９７】
また、図７のステップＴ３〜Ｔ４等に示したように、仮定式から結論式を直接導出する式が成立式群から除外されるので、順を追った論理的な解答を入力させることができる。従って、証明問題の学習効果を確実に高めることができる。
【００９８】
なお、上記の実施の形態における関数電卓１の各構成要素の細部構成及び細部動作に関しては、本発明の趣旨を逸脱しない範囲で適宜変更可能であることは勿論である。
【００９９】
例えば、本発明に係る計算装置を関数電卓１として説明したが、本発明が適用可能なものは、このような製品に限定されず、携帯電話、パソコン、ＰＤＡ（Ｐｅｒｓｏｎａｌ  Ｄｉｇｉｔａｌ  Ａｓｓｉｓｔａｎｔ）、ゲーム機などの電子機器全般に適用可能である。また、本発明に係る情報表示プログラム１３０は、関数電卓１に対して着脱可能なメモリカード、ＣＤ等に記憶されることとしてもよい。
【符号の説明】
【０１００】
１，１Ａ          関数電卓
２                入力キー群
３                ディスプレイ
１１              ＣＰＵ
１２              ＲＡＭ
１３              記憶部
１４              入力部
１５              表示部
１３０，１３０Ａ  情報表示プログラム
【図１】
2012137718.tif 000003
【図２】
2012137718.tif 000004
【図３】
2012137718.tif 000005
【図４】
2012137718.tif 000006
【図５】
2012137718.tif 000007
【図６】
2012137718.tif 000008
【図７】
2012137718.tif 000009