今年度研究の当初の目的は，以前に開発した数学教育システム calqid を，視覚化と証明記述も含めるように拡充するということであった．結果としては，証明記述用の iPad アプリケーションを，独立した形で開発したことが主な成果となった．
商学部の総合教育セミナーで，ペアノ算術に基づいた証明を書かせる訓練をしてきた．その際にいつも感じていたのは，存在例化による推論を習得させることの難しさである．これは，場合分けによる推論と共に，自然演繹で考えると，部分証明を要する推論パターンであり，それが理解と習得を困難にしていると思われる．
そこで，形式的な証明図ではなく，自然な記述スタイルで，なおかつ場合分けと存在例化を際立たせる証明を書かせるシステムを，iPad 用アプリケーションとして作成した．
比較的新しいインターフェイスである Swift UI を採用し，何ができて何ができないか，手探りしながらの作業となった．ペアノ算術の言語に限定して，一階述語論理での証明を，できるだけ自然な記述に合わせた形で作成するようにした．形式的に厳密に扱うと非常に煩瑣になる束縛変数の書き換えや，存在例化での自由変数の選択は自動化し，記述を簡素化するための仕組みを他にもいくつか組み込んである．Deduce for Peano Arithmetic という名前のアプリケーションとして，Apple Store での配布を準備している．
一方で，元々の calqid は，システムを一新し，calqitTutor という名称にした．それと並べて，商学部での中級微積分の授業で扱う3変数関数の条件付き極値問題を視覚化するページを付け加えた．
http://gentzen.hc.keio.ac.jp/calqitTutor/
http://gentzen.hc.keio.ac.jp/lagrangeX3d/
視覚化の仕組みは，非常に簡素なものである．3次元空間中での複数の等位面を，Python のライブラリ mayavi で生成させ，それをブラウザで表示可能な X3d ファイルにして表示している．
I developed an iPad application for writing proofs in Peano Arithmetic. Proofs in formal systems, such as sequent calculus and natural deduction, are often impractical in doing mathematics, especially in classroom environments, since they immediately become too formidable to comprehend the whole structure at a glance. On the other hand, informal proofs often suffer from the lack of transparency in the treatment of assumptions, which is particularly conspicuous in the use of subproofs in proof by cases and existential instantiation.
My intention is to develop a tool to help write handy proofs normally found in math textbooks, while making it explicit where and how subproofs are used. iPad seems the right platform for such a project.
The application is written in Swift and Swift UI, the Apple's new user interface. It has been a kind of struggle to find out what can and cannot be done in it. In any case, I have somehow managed to have it done, with some cozy apparatus for the automated variable renaming and so on. It is now in preparation for the distribution in Apple Store under the name Deduce for Peano Arithmetic.
Additionally, I extended my old web system for math education built on Django, with 3D-visualization for constrained-optimization problems, using MayaVi and X3dom via Python. Visit the following URLs:
http://gentzen.hc.keio.ac.jp/calqitTutor/
http://gentzen.hc.keio.ac.jp/lagrangeX3d/
The former is the old system updated, and the latter is newly added extension.
|
