How to Put Usability into Focus: Using Focus Groups to Evaluate the Usability of Interactive Theorem Provers

Bernhard Beckert
(Karlsruhe Institute of Technology (KIT))
Sarah Grebing
(Karlsruhe Institute of Technology (KIT))
Florian Böhl
(Karlsruhe Institute of Technology (KIT))

In recent years the effectiveness of interactive theorem provers has increased to an extent that the bottleneck in the interactive process shifted to efficiency: while in principle large and complex theorems are provable (effectiveness), it takes a lot of effort for the user interacting with the system (lack of efficiency). We conducted focus groups to evaluate the usability of Isabelle/HOL and the KeY system with two goals: (a) detect usability issues in the interaction between interactive theorem provers and their user, and (b) analyze how evaluation and survey methods commonly used in the area of human-computer interaction, such as focus groups and co-operative evaluation, are applicable to the specific field of interactive theorem proving (ITP).

In this paper, we report on our experience using the evaluation method focus groups and how we adapted this method to ITP. We describe our results and conclusions mainly on the ``meta-level,'' i.e., we focus on the impact that specific characteristics of ITPs have on the setup and the results of focus groups. On the concrete level, we briefly summarise insights into the usability of the ITPs used in our case study.

In Christoph Benzmüller and Bruno Woltzenlogel Paleo: Proceedings Eleventh Workshop on User Interfaces for Theorem Provers (UITP 2014), Vienna, Austria, 17th July 2014, Electronic Proceedings in Theoretical Computer Science 167, pp. 4–13.
Published: 29th October 2014.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: