| Budget Amount *help |
¥2,800,000 (Direct Cost: ¥2,800,000)
Fiscal Year 1998: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 1997: ¥1,200,000 (Direct Cost: ¥1,200,000)
Fiscal Year 1996: ¥800,000 (Direct Cost: ¥800,000)
|
|---|
| 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.
|
