Interactive Theorem Proving: An Empirical Study of User Activity

In this paper the interaction between users and the interactive theorem prover HOL is investigated from a human–computer interaction perspective. First, we outline three possible views of interaction, and give a brief survey of some current interfaces and how they may be described in terms of these views. Second, we describe and present the results of an empirical study of intermediate and expert HOL users. The results are analysed for evidence in support of the proposed view of proof activity in HOL. We believe that this approach provides a principled basis for the assessment and design of interfaces to theorem provers.