权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

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.

本研究的目的是设计和开发基于约束的文档编辑环境，从“人与计算机之间的协作”的观点，以支持人类的高度智能活动，如计算机代数，自动定理证明，和正式规格说明。描述使用计算机解决问题的结果的文档由将文档上的信息片段关联起来的约束组成，并且编辑这样的文档相当于定义和解决约束的活动。1996年，我们基于CAEP的思想，为计算机代数系统Mathematica设计并开发了一个用户界面，该界面是基于CAEP思想的。该接口在GNU Emacs上实现，用于编辑纯文本文档。我们还设计和开发了一个超文本文档的用户界面，描述了重写条款的过程。在1997年和1998年，为了支持不仅是长期重写，但也定理证明一般，我们设计和开发了一个用户界面HOL，在世界上广泛使用的通用定理证明助手。使用这个接口，当一个人正在编辑策略文本，一个人可以增量地执行文本的一部分，从定理证明助手的反馈可以反映在文本中。上述研究和发展意味着CAEP的思想是有效的，在高度智能活动，如计算机代数和定理证明。