Sciweavers

Share
CADE
2015
Springer

Interactive Theorem Proving - Modelling the User in the Proof Process

4 years 7 months ago
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.
Bernhard Beckert, Sarah Grebing
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where CADE
Authors Bernhard Beckert, Sarah Grebing
Comments (0)
books