{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:30:01Z","timestamp":1774837801872,"version":"3.50.1"},"reference-count":38,"publisher":"Oxford University Press (OUP)","issue":"6","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Interacting with Computers"],"published-print":{"date-parts":[[2000,7]]},"DOI":"10.1016\/s0953-5438(99)00023-5","type":"journal-article","created":{"date-parts":[[2002,7,25]],"date-time":"2002-07-25T13:57:26Z","timestamp":1027605446000},"page":"565-586","source":"Crossref","is-referenced-by-count":8,"title":["An analysis of errors in interactive proof attempts"],"prefix":"10.1093","volume":"12","author":[{"given":"S.","family":"Aitken","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"T.","family":"Melham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","reference":[{"issue":"4","key":"10.1016\/S0953-5438(99)00023-5_BIB1","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1145\/242223.242257","article-title":"Formal methods: state of the art and future directions","volume":"28","author":"Clarke","year":"1996","journal-title":"ACM Computing Surveys"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB2","series-title":"Isabelle: a generic theorem prover","author":"Paulson","year":"1994"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB3","series-title":"Introduction to HOL: a Theorem Proving Environment for Higher Order Logic","year":"1993"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB4","series-title":"Proceedings of the 11th Conference on Automated Deduction","first-page":"748","article-title":"PVS: a prototype verification system","author":"Owre","year":"1992"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB5","series-title":"Formal verification of the AAMP5 microprocessor: a case study in the industrial use of formal methods","author":"Miller","year":"1995"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB6","series-title":"A hybrid approach to verifying liveness in a symmetric multi-processor","author":"Camilleri","year":"1997"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB7","series-title":"Adding external decision procedures to HOL securely","author":"Gunter","year":"1998"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB8","unstructured":"A. Cant, M.A. Ozols, Xisabelle: a graphical user interface to the Isabelle theorem prover, Information Technology Division, DSTO, P.O. Box 1500, Salisbury, South Australia 5108, 1995."},{"key":"10.1016\/S0953-5438(99)00023-5_BIB9","series-title":"Higher Order Logic Theorem Proving and its Applications","first-page":"115","article-title":"A proof development system for the HOL theorem prover","author":"Th\u00e9ry","year":"1994"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB10","series-title":"Higher Order Logic Theorem Proving and its Applications","first-page":"324","article-title":"A new interface for HOL: ideas, issues, and implementation","author":"Syme","year":"1995"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB11","series-title":"User Interfaces for Theorem Provers: UITP\u201996","article-title":"The CtCoq experience","author":"Bertot","year":"1996"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB12","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1006\/jsco.1997.0171","article-title":"A generic approach to building user interfaces for theorem provers","volume":"25","author":"Bertot","year":"1998","journal-title":"Journal of Symbolic Computation"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB13","series-title":"User Interfaces for Theorem Provers: UITP\u201996","article-title":"Jape's quiet interface","author":"Bornat","year":"1996"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB14","series-title":"Implementing proof by pointing without a structure editor","author":"Bertot","year":"1997"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB15","series-title":"The Psychology of Everyday Things","author":"Norman","year":"1988"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB16","unstructured":"N.A. Merriam, A.M. Dearden, M.D. Harrison, Assessing theorem proving assistants: concepts and criteria, Proceedings of the Workshop on User Interface Design for Theorem Proving Systems, Department of Computing Science, Glasgow, 1995"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB17","unstructured":"J. Rasmussen, A. Pejtersen, K. Schmidt, Taxonomy for cognitive work analysis, Technical Report M-2871, Riso National Laboratory, Roskilde, Denmark, September 1990."},{"key":"10.1016\/S0953-5438(99)00023-5_BIB18","doi-asserted-by":"crossref","first-page":"277","DOI":"10.1016\/0743-1066(88)90001-5","article-title":"The transparent Prolog machine (TPM): an execution model and graphical debugger for logic programming","volume":"5","author":"Eisenstadt","year":"1988","journal-title":"Journal of Logic Programming"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB19","series-title":"Proceedings of the Fifth International Conference Symposium on Logic Programming","article-title":"Adding data and procedure abstraction to the Transparent Prolog Machine (TPM)","author":"Brayshaw","year":"1988"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB20","doi-asserted-by":"crossref","unstructured":"H. Lieberman, C. Fry, Bridging the gulf between code and behaviour in programming, Proceedings of ACM Conference of Human Factors and Computing Systems (CHI) Denver, 1995, 480\u2013486.","DOI":"10.1145\/223904.223969"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB21","series-title":"Software Visualization: Programming as a Mutli-media Experience","first-page":"439","article-title":"A principled approach to the evaluation of software visualization: a case-study in Prolog","author":"Mullholland","year":"1998"},{"issue":"4","key":"10.1016\/S0953-5438(99)00023-5_BIB22","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1080\/10447319209526046","article-title":"Errors in working with office computers: a first validation of a taxonomy for observed errors in a field setting","volume":"4","author":"Zapf","year":"1992","journal-title":"International Journal of Human\u2013Computer Interaction"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB23","series-title":"XBarnacle: making theorem provers more accessible","author":"Lowe","year":"1997"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB24","series-title":"Supplementary Proceedings of the Seventh International Workshop on Higher Order Logic Theorem Proving and its Applications, University of Malta, Valletta, September 1994","article-title":"A tree-based, graphical interface for large proof development","author":"Schubert","year":"1994"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB25","series-title":"Proceeding of the Third Conference on Rewriting Techniques and Applications","first-page":"137","article-title":"An overview of LP: the Larch Prover","author":"Garland","year":"1993"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB26","series-title":"Edinburgh LCF: a Mechanised Logic of Computation","author":"Gordon","year":"1979"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB27","first-page":"31","article-title":"A virtual protocol model for human\u2013computer interaction","volume":"24","author":"Neilsen","year":"1986","journal-title":"International Journal of Man\u2013Machine Studies"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB28","series-title":"User Centred System Design","article-title":"Direct manipulation interfaces","author":"Hutchins","year":"1986"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB29","doi-asserted-by":"crossref","first-page":"263","DOI":"10.1006\/jsco.1997.0175","article-title":"Interactive theorem proving: a study of user activity","volume":"25","author":"Aitken","year":"1998","journal-title":"Journal of Symbolic Computation"},{"issue":"3","key":"10.1016\/S0953-5438(99)00023-5_BIB30","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1016\/S0020-7373(74)80027-1","article-title":"Human errors in programming","volume":"6","author":"Youngs","year":"1974","journal-title":"International Journal of Man\u2013Machine Studies"},{"issue":"1","key":"10.1016\/S0953-5438(99)00023-5_BIB31","doi-asserted-by":"crossref","first-page":"119","DOI":"10.1016\/S0020-7373(77)80046-1","article-title":"Reducing programming errors in nested conditionals by prescribing a writing procedure","volume":"9","author":"Sime","year":"1977","journal-title":"International Journal of Man\u2013Machine Studies"},{"issue":"4","key":"10.1016\/S0953-5438(99)00023-5_BIB32","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1016\/S0020-7373(83)80059-5","article-title":"User error or computer error? Observations on a statistics package","volume":"19","author":"Davis","year":"1983","journal-title":"International Journal of Man\u2013Machine Studies"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB33","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1037\/0033-295X.88.1.1","article-title":"Categorisation of action slips","volume":"88","author":"Norman","year":"1981","journal-title":"Psychological Review"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB34","series-title":"Explorations in Human\u2013Computer Interaction and Artificial Intelligence","article-title":"Errors in an interactive programming environment: causes and cures in novice programming environments","author":"Eisenstadt","year":"1992"},{"issue":"6","key":"10.1016\/S0953-5438(99)00023-5_BIB35","doi-asserted-by":"crossref","first-page":"561","DOI":"10.1016\/S0020-7373(83)80071-6","article-title":"Task analysis and user errors: a methodology for assessing interactions","volume":"19","author":"Davis","year":"1983","journal-title":"International Journal of Man\u2013Machine Studies"},{"issue":"1","key":"10.1016\/S0953-5438(99)00023-5_BIB36","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0020-7373(81)80022-3","article-title":"The command language grammar: a representation for the user interface of interactive computer systems","volume":"15","author":"Moran","year":"1981","journal-title":"International Journal of Man\u2013Machine Studies"},{"issue":"4","key":"10.1016\/S0953-5438(99)00023-5_BIB37","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1080\/10447319009525988","article-title":"Identifying and interpreting design errors","volume":"2","author":"Booth","year":"1990","journal-title":"International Journal of Human\u2013Computer Interaction"},{"key":"10.1016\/S0953-5438(99)00023-5_BIB38","article-title":"ITP Project Anthology, Technical Report TR\u20131997\u201336","author":"Aitken","year":"1997","journal-title":"Department of Computing Science, University of Glasgow"}],"container-title":["Interacting with Computers"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/iwc\/article-pdf\/12\/6\/565\/2061301\/iwc12-0565.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T21:23:41Z","timestamp":1578518621000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/iwc\/article-lookup\/doi\/10.1016\/S0953-5438(99)00023-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,7]]},"references-count":38,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2000,7]]}},"alternative-id":["S0953543899000235"],"URL":"https:\/\/doi.org\/10.1016\/s0953-5438(99)00023-5","relation":{},"ISSN":["0953-5438"],"issn-type":[{"value":"0953-5438","type":"print"}],"subject":[],"published":{"date-parts":[[2000,7]]}}}