人間と計算機の協調の視点に立った問題解決のための文書編集環境

1997 Fiscal Year Annual Research Report

• Project/Area Number: 08680348
• Research Category: Grant-in-Aid for Scientific Research (C)
• Research Institution: The University of Tokyo
• Principal Investigator: 萩谷 昌己 東京大学, 大学院・理学系研究科, 教授 (30156252)
• Keywords: ユーザインタフェース / 文書編集 / 制約 / ハイパーテキスト / 定理証明 / 項書き換え / タクティク

Research Abstract

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

Research Products

• [Publications] Yasuaki Takabe & Masami Hagiya: "A User Interface for Controlling Term Rewriting Based on Computing-as Editing Pardigm" User Interface for Theorem Provers. 93-100 (1997)
• [Publications] 萩谷昌己・高橋孝一: "「計算=編集」パラダイムに従うHOLタクティクのためのEmacsインタフェース" レクチャーノート/ソフトウェア学(近代科学社)インタラクティブシステムとソフトウェアV. 18. 123-128 (1997)