Real theorem provers deserve real user-interfaces
Laurent Théry, Yves Bertot, Gilles Kahn · 1992
This paper explains how to add a modern user interface to existing theorem provers, using principles and tools designed for programming environments. 1 Introduction There are a number of reasons for which it is interesting to build better user interfaces for theorem proving systems, i.e., computer systems that assist in making formal deductions. ffl First the user-interface of today's theorem proving systems is generally very weak. This is in contrast with many other facets that have matured considerably in the last ten years. Notable user-interface experiments are (IPE[Ritchie88], Mural[Jones91], KIDS[Smith90]) but they put forward simultaneously a new logical system and a new interface that are closely intertwined. ffl Proving theorems is an exemplary symbolic activity. It is generally accepted that a cooperation between the user and the computer is mandatory, even though some subtasks may be handled entirely automatically. In comparison to symbolic algebra systems, such as Mathem...