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

1996 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の考えに基づいて、数式処理系であるMathematicaのために、GNU Emacs上にプレーン・テキストに対するユーザ・インターフェースを設計・実現した。この仕事とわれわれが従来より開発して来た証明検査系のユーザ・インターフェースの仕事をまとめ、ヨ-ク大学で行われた国際ワークショップにおいて発表した。
上述の数式処理系および証明検査系のユーザ・インタフェースはともにプレーン・テキストに対するものであった。本年度は、それとあわせて、ハイパーテキストに対するユーザ・インターフェースの設計・実現も行った。この仕事では、ユーザ・インターフェースの対象として項の書き換え系を選んだ。項の書き換えは、数式処理においても定理証明においても、最も基本的な推論方式である。本研究では、項の書き換え関係を文書内の制約として記述できるようにハイパーテキスト記述言語であるHTMLを拡張し、拡張されたHTMLを編集するためのユーザ・インタフェースを設計・実現した。また、CAEPの考えの観点より、プレーン・テキストとハイパーテキストの比較等を行った。以上の仕事については、日本ソフトウェア科学会のインタラクティブシステムとソフトウェアに関するワークショップにて発表した。

Research Products

• [Publications] Masami Hagiya & Hiroshi Kakuno: "Proring as Editing" User Interfaces for Theovem Provers. 35-42 (1996)
• [Publications] 竹辺靖昭・萩谷昌己: "CAEPに基づいた項書き換え制御のユーザインターフェース" レクチャーノート/ソフトウェア学(近代科学社)インタラクティブシステムとソフトウェアIV. 16. 31-40 (1996)