UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

Reasoning about order errors in interaction

Curzon, P.; Blandford, A.E.; (2000) Reasoning about order errors in interaction. In: Aagaard, M. and Harrison, J. and Schubert, T., (eds.) Supplemental proceedings of the 13th international conference on theorem proving in higher order logics (TPHOLs 2000). (pp. pp. 33-48). Oregon Graduate Institute: Portland, US. Green open access

[img]
Preview
PDF - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
701Kb

Abstract

Reliability of an interactive system depends on users as well as the device implementation. User errors can result in catastrophic system failure. However, work from the field of cognitive science shows that systems can be designed so as to completely eliminate whole classes of user errors. This means that user errors should also fall within the remit of verification methods. In this paper we demonstrate how the HOL theorem prover [7] can be used to detect and prove the absence of the family of errors known as order errors. This is done by taking account of the goals and knowledge of users. We provide an explicit generic user model which embodies theory from the cognitive sciences about the way people are known to act. The user model describes action based on user communication goals. These are goals that a user adopts based on their knowledge of the task they must perform to achieve their goals. We use a simple example of a vending machine to demonstrate the approach. We prove that a user does achieve their goal for a particular design of machine. In doing so we demonstrate that communication goal based errors cannot occur.

Type:Proceedings paper
Title:Reasoning about order errors in interaction
Open access status:An open access version is available from UCL Discovery
Publisher version:http://content.ohsu.edu/cdm4/item_viewer.php?CISOROOT=/csetech&CISOPTR=272&CISOBOX=1&REC=12
Language:English
Additional information:Paper given at the 13th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2000) held at Portland, Oregon, USA, August 14-18 2000, and published as part of the supplemental proceedings. The main proceedings volume is published by Springer in 'Lecture Notes in Computer Science', Vol. 1869 http://www.springer.com/computer/foundations/book/978-3-540-67863-2
UCL classification:UCL > School of Life and Medical Sciences > Faculty of Brain Sciences > Psychology and Language Sciences (Division of) > UCL Interaction Centre

View download statistics for this item

Archive Staff Only: edit this record