Document Editing Environment for Problem Solving from the Viewpoint of Collaboration between Humans and Computers

从人机协作的角度解决问题的文档编辑环境

基本信息

批准号：
08680348
负责人：
HAGIYA Masami
金额：
$ 1.79万
依托单位：
The University of Tokyo
依托单位国家：
日本
项目类别：
Grant-in-Aid for Scientific Research (C)
财政年份：
1996
资助国家：
日本
起止时间：
1996 至 1998
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-08680348/
关键词：
user-interface document editing constraint hypertext computer algebra theorem proving term rewriting タクティク

项目摘要

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.

这项研究旨在从“人与计算机之间的协作”的角度设计和开发基于约束的文档编辑环境，以支持人类的高度智力活动，例如计算机代数，自动化定理证明和正式规范。描述使用计算机解决问题的结果的文档由将文档中信息段的限制组成，并编辑此类文档与定义和求解约束的活动相当。根据我们将计算范式（CAEP）命名为“计算”的工作假设，定义约束被视为编程，并将约束求解为计算。在1996年，基于CAEP的概念，我们根据计算机代数系统为Mathematica设计和开发了Mathematica的用户界面。该界面在GNU emacs上实现，并用于编辑纯文本文档。我们还为超文本文档设计并开发了一个用户界面，以描述重写术语的过程。在1997年和1998年，为了不仅支持术语重写，而且还证明了定理，我们为HOL设计并开发了一个用户界面，HOL是一种通用定理，证明助手在世界范围内广泛使用。使用此界面，在编辑策略文本的同时，可以逐步执行文本的一部分，并且可以反映出定理证明助手的反馈。