Abstract:
This paper discusses some observations on the differences between what the designers of theorem proving assistants (TPAs) think about the systems they designed and what the users of those TPAs actually find. A questionnaire based on the cognitive dimensions framework was sent to designers and users of a sample of TPAs. The aim of this work is to be able to identify specific areas that designers of TPAs need to devote extra attention to. It was observed that the cognitive dimensions of closeness of mapping, visibility and juxtaposability and perceptual cues are of particular significance.
PPIG 2000 - 12th Annual Workshop
A Cognitive Dimensions view of the differences between designers and users of theorem proving assistants