「ロボットは数学の大学入試問題をどうやって解くか？」

このたび、千葉県高等学校教育研究会数学部会の平成29年度総会・春季研究大会において、標記の講演の機会をいただきました。

今回の会場は千葉県茂原市の千葉県立長生高校で、今年創立130周年を迎えるという伝統校です。最初、このお話をいただいた際に、過去の講演者のリスト（部会のホームページに過去の記録が掲載されています）を見たところ、錚々たる顔ぶれで、自分も話を聴きたいような先生方ばかりでした。そのような中で、自分にどんな話ができるだろうと考えた結果、これまで共同研究に参加させていただいている「東ロボ」に関連し、数式処理で数学の演習／入試問題を解く手法の紹介を行うことにしました。

講演では、「東ロボ」のプロジェクトの概要の紹介、数学ソルバによる解答の流れの紹介を行った後、「実閉体上の一階述語論理式の量化子消去 (Quantifier Elimination; QE)」に焦点を当て、「実閉体上の一階述語論理式」とはどんなものか、QEとはどのようなことを行うものかを紹介しました。この中では、オンラインで使える数式処理システム CoCalc 上で、QEパッケージの QEPCAD を使ったQEの計算も紹介しました。本当は直接オンラインでデモンストレーションをやりたかったのですが、残念ながらインターネット接続がうまくいかなかったので、あらかじめファイルに保存しておいた計算セッションを見せながら紹介しました。

そして、QEの汎用アルゴリズムの一つである Cylindrical Algebraic Decomposition (CAD) の紹介を行いました。もちろんCADの全体像を説明する時間はありませんから、今回は、CADの要素として、1) 与えられた多項式の値が正、0、負になる領域を調べること、2) しかし、各変数ごとにすべての値を調べるのは原理的に無理なので、与えられた多項式の実零点が重なったり、実零点の個数が変化したりする特徴的な部分を調べること、3) そのために、与えられた多項式の終結式や判別式を求めること、4) その上で、1変数代数方程式の実零点の数え上げを行うこと、を説明しました。そして、1変数代数方程式の実零点の数え上げの方法としてSturm法を紹介しました。

こんな形で今回の講演を行いましたが、講演後の高校の先生方との意見交換では、いろいろと貴重なお話も伺い、大変有意義な時間になりました。今回、このような機会を作ってくださった皆様に感謝申し上げます。なお、今回のような内容の講演や、この内容に興味／関心を持つ高校生の人達とのQE計算の実習など、ご希望がございましたら、時間が許す範囲でお応えしたいと思います。