Research Output

Using ERMIA for the Evaluation of a Theorem Prover Interface

  ERMIA (Entity-Relationship Modelling of Information Artefacts) provides an extension to entity-relationship
modelling techniques to provide a structural representation of the interaction between people and “information
artefacts”. Such a representation may then be used to compare contrasting interface designs or identify potential
usability problems in an existing system. In this paper we present an application of ERMIA analysis to a version
of the XBarnacle semi-automated theorem proving system that features interactive proof critics

  • Type:

    Book Chapter

  • Date:

    30 November 2003

  • Publication Status:


  • Publisher


  • Library of Congress:

    QA Mathematics

  • Dewey Decimal Classification:

    511 General principles of mathematics


Jackson, M., Benyon, D. & Lowe, H. (2003). Using ERMIA for the Evaluation of a Theorem Prover Interface. In Backhouse, R. (Ed.). Proceedings of the 4th International Workshop on User Interfaces for Theorem Provers, 104-111. UITP



Entity-relationship modelling; information artefacts; interface design; usability; ERMIA; XBarnacle; semi-automated theorem prover;

Available Documents