|
本研究の目的は、数式処理、定理証明、形式的仕様記述など、人間の高度に知的な活動を必要とする分野に対して、「人間と計算機の協調」の視点に立った編集環境を制約の概念を用いて設計・実現することにある。計算機上での問題解決の結果を表現した文書上の情報は、その中で互いに様々な制約関係によって結びついており、このような文書の編集は制約の設定とその解消の作業から成り立っている。文書上の制約の設定をプログラミング、その制約の解消を計算ととらえる考えを、我々はComputing-as-Editing Paradigm (CAEP)と名づけている。
平成8年度は、まず、CAEPの考えに基づいて、数式処理系であるMathematicaのために、GNU Emacs上にプレーン・テキストに対するユーザ・インターフェースを設計・実現した。それとあわせて、項の書き換えの過程を記述するハイパーテキストに対するユーザ・インターフェースの設計・実現も行った。平成9年度より平成10年度にかけて、項の書き換えに限らず、証明活動を幅広く支援するために、世界で最もよく使われている汎用の証明支援系であるHOLのためのユーザ・インタフェースを設計・開発した。このインターフェースでは、タクティクのテキストを編集しながらインクリメンタルにその一部を実行し、証明支援系からのフィードバックをテキストに反映させることができる。
以上の研究と開発により、CAEPの考えが、数式処理や定理証明などの高度に知的な作業において有効であることが実証されたと考えられる。
|
