Interactive Theorem Proving - Modelling the User in the Proof Process

Proving complex problems requires user interaction during proof construction. A major prerequisite for user interaction is that the user is able to understand the proof state in order to guide the prover in finding a proof. Previous evaluations using focus groups for two interactive theorem provers have shown that there exists a gap between the user’s model of the proof and the actual proof performed by the provers’ strategies. In this paper, we sketch a process model of the interactive proof process that helps to analyze this gap. Additionally, we give insight into the results of a usability test of the interactive verification System KeY, which provides evidence that this model is consistent with the actual proof process.

• Type: Journal
• Year: 2015
• Where: CADE
• Authors: Bernhard Beckert, Sarah Grebing
• Keywords: CADE 2015, Logical Reasoning