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

本研究旨在从“人机协作”的角度设计和开发基于约束的文档编辑环境，以支持计算机代数、自动定理证明和形式化规范等人类高度智能的活动。描述使用计算机解决问题的结果的文档由与文档上的信息片段相关的约束组成，编辑这样的文档相当于定义和解决约束的活动。根据这一工作假设，我们将其命名为计算即编辑范式（CAEP），定义约束被认为是编程，求解约束被认为是计算。1996年，基于CAEP的思想，我们为计算机代数系统Mathematica设计并开发了一个用户界面。该接口是在GNU Emacs上实现的，用于编辑纯文本文档。我们还设计并开发了一个用于描述重写术语过程的超文本文档的用户界面。在1997年和1998年，为了支持术语重写和一般定理证明，我们设计并开发了一个用户界面，用于HOL，一个在世界上广泛使用的通用定理证明助手。使用该界面，在编辑策略文本时，可以增量执行文本的一部分，定理证明助手的反馈可以反映在文本中。上述研究和发展表明，CAEP思想在计算机代数和定理证明等高智力活动中是有效的。

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.