User Interfaces for Theorem Provers: Necessary Nuisanec or Unexplored Potential?

Christoph Lüth

In: Ninth International Workshop on Automated Verification of Critical Systems (AVOCS'09). Workshop on Automated Verification of Critical Systems (AVOCS-09) 9th September 23-25 Swansea United Kingdom Electronic Communications of the EASST 23 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.

Weitere Links

main-final.pdf (pdf, 123 KB)

German Research Center for Artificial Intelligence
Deutsches Forschungszentrum für Künstliche Intelligenz