Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1007/978-3-319-15201-1_1 | Lecture Notes in Computer Science |
Field | DocType | Volume |
Theorem provers,Bottleneck,Obstacle,Systems engineering,Software engineering,Computer science,Usability,Bridging (networking),Theoretical computer science,Proof obligation,Gas meter prover,Focus group | Conference | 8938 |
ISSN | Citations | PageRank |
0302-9743 | 7 | 0.58 |
References | Authors | |
6 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Bernhard Beckert | 1 | 862 | 86.50 |
| Sarah Grebing | 2 | 72 | 4.57 |
| Florian Böhl | 3 | 7 | 0.58 |