Analysis of errors in interactive proof attempts

Citations of this article
Mendeley users who have this article in their library.


The practical utility of interactive, user-guided, theorem proving depends on the design of good interaction environments, the study of which should be grounded in methods of research into human-computer interaction (HCI). This paper discusses the relevance of classifications of programming errors developed by the HCI community to the problem of interactive theorem proving. A new taxonomy of errors is proposed for interaction with theorem provers and its adequacy as a usability metric is assessed experimentally.




Aitken, S., & Melham, T. (2000). Analysis of errors in interactive proof attempts. Interacting with Computers, 12(6), 565–586.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free