A Usability Evaluation of Interactive Theorem Provers Using Focus Groups

摘要

The effectiveness of interactive theorem provers (ITPs) increased such that the bottleneck in the proof process shifted from effectiveness to efficiency. While in principle large theorems are provable, it takes much effort for the user to interact with the system. A major obstacle for the user is to understand the proof state in order to guide the prover in successfully finding a proof. We conducted two focus groups to evaluate the usability of ITPs. We wanted to evaluate the impact of the gap between the user's model of the proof and the actual proof performed by the provers' strategies. In addition, our goals are to explore which mechanisms already exist and to develop, based on the existing mechanisms, new mechanisms that help the user in bridging this gap.