A Generic Approach to Building User Interfaces for Theorem Provers

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.