| 研究課題/領域番号 |
08680348
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
計算機科学
|
|---|
| 研究機関 | 東京大学 |
|---|
研究代表者 |
萩谷 昌己 東京大学, 大学院・理学系研究科, 教授 (30156252)
|
|---|
| 研究期間 (年度) |
1996 – 1998
|
| 研究課題ステータス |
完了 (1998年度)
|
| 配分額 *注記 |
2,800千円 (直接経費: 2,800千円)
1998年度: 800千円 (直接経費: 800千円)
1997年度: 1,200千円 (直接経費: 1,200千円)
1996年度: 800千円 (直接経費: 800千円)
|
|---|
| キーワード | ユーザインタフェース / 文書編集 / 制約 / ハイパーテキスト / 数式処理 / 定理証明 / 項書き換え / タクティク |
|---|
| 研究概要 |
本研究の目的は、数式処理、定理証明、形式的仕様記述など、人間の高度に知的な活動を必要とする分野に対して、「人間と計算機の協調」の視点に立った編集環境を制約の概念を用いて設計・実現することにある。計算機上での問題解決の結果を表現した文書上の情報は、その中で互いに様々な制約関係によって結びついており、このような文書の編集は制約の設定とその解消の作業から成り立っている。文書上の制約の設定をプログラミング、その制約の解消を計算ととらえる考えを、我々はComputing-as-Editing Paradigm (CAEP)と名づけている。
平成8年度は、まず、CAEPの考えに基づいて、数式処理系であるMathematicaのために、GNU Emacs上にプレーン・テキストに対するユーザ・インターフェースを設計・実現した。それとあわせて、項の書き換えの過程を記述するハイパーテキストに対するユーザ・インターフェースの設計・実現も行った。平成9年度より平成10年度にかけて、項の書き換えに限らず、証明活動を幅広く支援するために、世界で最もよく使われている汎用の証明支援系であるHOLのためのユーザ・インタフェースを設計・開発した。このインターフェースでは、タクティクのテキストを編集しながらインクリメンタルにその一部を実行し、証明支援系からのフィードバックをテキストに反映させることができる。
以上の研究と開発により、CAEPの考えが、数式処理や定理証明などの高度に知的な作業において有効であることが実証されたと考えられる。
|
