A Generic Approach to Building User Interfaces for Theorem Provers
A Generic Approach to Building User Interfaces for Theorem Provers
复制标题
为定理证明者构建用户界面的通用方法
DOI：
10.1006/jsco.1997.0171
复制
发表时间：
1998
期刊：
影响因子：
--
通讯作者：
L. Théry
中科院分区：
文献类型：
--
作者：
Yves Bertot;L. Théry
在本文中，我们展示了为证明系统构建用户界面所做的持续努力的结果。我们的方法是通用的：我们不是为特定的证明系统构建用户界面，而是开发了已应用于多个证明系统的技术和工具。我们首先提出并激发了一种分布式架构，其中证明系统和接口是通过协议进行通信的两个独立进程。然后我们描述三个高级功能：指向证明、脚本管理和文本解释。总而言之，它们利用了底层架构并产生了更加用户友好的证明环境。
In this paper, we present the results of an ongoing effort in building user interfaces for proof systems. Our approach is generic: we are not constructing a user interface for a particular proof system, rather we have developed techniques and tools that have been applied to several proof systems. We first propose and motivate a distributed architecture, where the proof system and the interface are two separate processes communicating through a protocol. Then we describe three high-level features:proof-by-pointing,script management, andtextual explanation. Altogether, they take advantage of the underlying architecture and yield a more user-friendly proof environment.