User Interfaces for Theorem Provers: Necessary Nuisance or Unexplored Potential?
Christoph Lüth · Technische Universität Berlin – Universitätsbibliothek · 2009
This note considers the design of user interfaces for interactive theorem provers. The basic rules of interface design are reviewed, and their applicability to theorem provers is discussed, leading to considerations about the particular challenges of interface design for theorem provers. A short overview and classification of existing interfaces is given, followed by suggestions of possible future work in the area.