1998 Fiscal Year Final Research Report Summary
Document Editing Environment for Problem Solving from the Viewpoint of Collaboration between Humans and Computers
| Project/Area Number |
08680348
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | The University of Tokyo |
|---|
Principal Investigator |
HAGIYA Masami The University of Tokyo, Department of Information Science, Professor, 大学院・理学系研究科, 教授 (30156252)
|
|---|
| Project Period (FY) |
1996 – 1998
|
| Keywords | user-interface / document editing / constraint / hypertext / computer algebra / theorem proving / term rewriting |
|---|
| Research Abstract |
This research aims at designing and developing constraint-based document editing environments from the viewpoint of "collaboration between humans and computers" for supporting highly intellectual activities of humans such as computer algebra, automated theorem proving, and formal specification. A document that describes the results of solving a problem using computers consists of constraints that relate pieces of information on the document, and editing such a document amounts to activities of defining and solving constraints. According to this working hypothesis, which we named Computing-as-Editing Paradigm (CAEP), defining constraints is considered as programming, and solving the constraints as computation.
In 1996, based on the idea of CAEP, we designed and developed a user-interface for Mathematica, a computer algebra system. The interface is implemented on GNU Emacs and used to edit plain text documents. We also designed and developed a user-interface for hypertext documents that describe a process of rewriting terms. In 1997 and 1998, in order to support not only term rewriting but also theorem proving in general, we designed and developed a user-interface for HOL, a general-purpose theorem proving assistant widely used in the world. Using this interface, while one is editing tactic text, one can incrementally execute a part of the text and the feedback from the theorem proving assistant can be reflected in the text.
The above research and development imply that the idea of CAEP is effective in highly intellectual activities such as computer algebra and theorem proving.
|
Research Products
(12 results)
