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