Evaluating the Interfaces of Three Theorem Proving Assistants

  • Nicholas A. Merriam
  • Michael D. Harrison
Part of the Eurographics book series (EUROGRAPH)


A first step in systematically engineering better interfaces for theorem proving assistants (TPAs) is to assess what has already been achieved in the domain. We examine three TPAs employing quite different styles of interaction. We consider the support provided by the interfaces for each of four mechanisms for efficient interactive proof: planning, reuse, reflection and articulation. Common themes are observed, as are strengths and weaknesses of the interfaces and we discuss the general issues, attempting to abstract away from the particular artifacts studied.


Inference Rule Theorem Prove Interaction Style Current Goal Proof Tree 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    J. S. Aitken, P. Gray, T. Melham, and M. Thomas. A Study of User Activity in Interactive Theorem Proving. Submitted to J. Symbolic Computing.Google Scholar
  2. 2.
    W. M. Farmer, J. D. Guttman, and F. J. Thayer. Little theories. In Kapur [8], pages 567–581.Google Scholar
  3. 3.
    W. M. Farmer, J. D. Guttman, and F. J. Thayer. The IMPS User’s Maunual. The MITRE Corporation, 1994.Google Scholar
  4. 4.
    G. Gentzen. Investigations into logical deduction. In M. E. Szabo, editor, The Collected Papers of Gerhard Gentzen. North-Holland, 1969.Google Scholar
  5. 5.
    D. J. Gilmore. Structural Visibility and Program Comprehension. In M. D. Harrison and A. F. Monk, editors, People and Computers: Designing for Usability, BCS Workshop series, pages 527–545. Cambridge University Press, 1986.Google Scholar
  6. 6.
    Li Gong, Patrick Lincoln, and John Rushby. Byzantine agreement with authentication: Observations and applications in tolerating hybrid and link faults. In Dependable Computing for Critical Applications—5, pages 79–90, Champaign, IL, September 1995. IFIP WG 10.4, preliminary proceedings.Google Scholar
  7. 7.
    J.-M. Hoc, T. R. G. Green, R. Samurçay, and D. J. Gilmore, editors. Psychology of Programming. Computers and People. Academic Press, 1990.Google Scholar
  8. 8.
    D. Kapur, editor. Automated Deduction — CADE 11, volume 607 of Lecture Notes in Computer Science. Springer-Verlag, 1992.Google Scholar
  9. 9.
    D. Kirshner. The Visual Syntax of Algebra. Journal for Research in Mathematical Education, 20(3):274–287, 1989.CrossRefGoogle Scholar
  10. 10.
    Leslie Lamport. How to Write a Long Formula. Online at, 1993.Google Scholar
  11. 11.
    J. H. Larkin and H. A. Simon. Why a Diagram is (Sometimes) Worth Ten Thousand Words. Cognitive Science, 11:65–99, 1987.CrossRefGoogle Scholar
  12. 12.
    W. N. Dember and J. S. Warm. Psychology of Perception, chapter 7: Perception of Form. Holt, Rinehart and Winston, 1979.Google Scholar
  13. 13.
    W. M. Newman and M. G. Lamming. Interactive System Design. Addison-Wesley, 1995.Google Scholar
  14. 14.
    J. Nicholls. Z Notation: version 1.2. Technical report, Z Standards Panel, University of Oxford, Sept. 1995.Google Scholar
  15. 15.
    D. C. Oppen. Pretty-printing. ACM Transactions on Programming Languages, 2(4), Oct. 1980.Google Scholar
  16. 16.
    S._Owre, J. Rushby, and N. Shankar. PVS: A Prototype Verification System. In Kapur [8], pages 748–752.Google Scholar
  17. 17.
    Philippe Palanque. Towards an integrated proposal for Interactive Systems design based on TLIM and ICO. In F. Bodart and J. Vanderdonckt, editors, Eurographics Workshop on Design, Specification and Verification of Interactive Systems: Informal Proceedings, pages 69–85, Belgium, 1996. Computer Science Dept. U. Namur.Google Scholar
  18. 18.
    G. Polya. How To Solve It. Princeton University Press, second edition, 1957.Google Scholar
  19. 19.
    J. Rasmussen. Skills, Rules and Knowledge; signals, signs and symbols, and other distinctions in human performance models. IEEE Transactions on Systems, Man and Cybernetics, 13(3):257–266, 1983.Google Scholar
  20. 20.
    John Rushby. Design choices in specification languages and verification systems. In Phillip Windley, editor, International Workshop on the HOL Theorem Proving System and its Applications, pages 195–204. IEEE Computer Society, 1991.Google Scholar
  21. 21.
    N. Shankar, S. Owre, and J. Rushby. The PVS Proof Checker: A Reference Manual SRI International, 1995.Google Scholar
  22. 22.
    R. Shostak. On the SUP-INF method for proving Presburger formulas. Journal of the ACM, 24(4):529–543, Oct. 1977.CrossRefMATHMathSciNetGoogle Scholar
  23. 23.
    J. M. Spivey. The Z Notation. Prentice Hall International, 2nd edition, 1992.Google Scholar
  24. 24.
    E. Swanson. Mathematics into Type. American Mathematical Society, 1971.Google Scholar
  25. 25.
    I. Toyn and J. Hall. Proving Conjectures using Cadiz. University of York, 1995.Google Scholar
  26. 26.
    J. C. P. Woodcock and S. M. Brien. W: A logic for Z. In J. E. Nicholls, editor, Z User Workshop, York 1991, Workshops in Computing, pages 77–96. Springer-Verlag, 1992.Google Scholar

Copyright information

© Springer-Verlag/Wien 1996

Authors and Affiliations

  • Nicholas A. Merriam
    • 1
    • 2
  • Michael D. Harrison
    • 1
  1. 1.Department of Computer ScienceUniversity of YorkHeslington, YorkUK
  2. 2.EPSRC grant GR/K09205UK

Personalised recommendations