A Theoretical Analysis of Hierarchical Proofs

  • Paul Cairns
  • Jeremy Gow
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2594)


Hierarchical proof presentations are ubiquitous within logic and computer science,but have made little impact on mathematics in general.The reasons for this are not currently known,and need to be understood if mathematical knowledge management systems are to gain acceptance in the mathematical community.We report on some initial experiments with three users of a set of web-based hierarchical proofs, which suggest that usability problems could be a factor.In order to better understand these problems we present a theoretical analysis of hierarchical proofs using Cognitive Dimensions [6].The analysis allows us to formulate some concrete hypotheses about the usability of hierarchical proof presentations.


Usability Problem Cognitive Dimension Mental Workload Proof Step Progressive Evaluation 
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.
    R. Bornat, B. Sufrin,‘Animating Formal Proofs at the Surface:The Jape Proof Calculator,’ The Computer Journal,42(3):177–192,1999CrossRefGoogle Scholar
  2. 2.
    P. Cairns, J. Gow,“On Dynamically Presenting a Topology Course,” First Interna-tional Workshop on Mathematical Knowledge Management,2001.Revised version submitted to Annals of A.I.& Math.,2002Google Scholar
  3. 3.
    K. Easthaughffe,‘Support for Interactive Theorem Proving:Some Design Princi-ples and Their Application,’ in R. Backhouse (ed.),Workshop on User Interfaces for Theorem Provers,p 96–103,1998Google Scholar
  4. 4.
    X. Faulkner, Usability Engineering, Palgrave, 2002Google Scholar
  5. 5.
    T.R.G. Green, A. Blackwell, A tutorial on cognitive dimensions,
  6. 6.
    T.R.G. Green, M. Petre,‘Usability analysis of visual programming environments: a “cognitive dimensions ” framework,’ J.Visual Languages and Computing,7:131–174,1996CrossRefGoogle Scholar
  7. 7.
    J. Grundy,‘A Browsable Format for Proof Presentation,’ Math.Universalis, 2, 1996,
  8. 8.
    P.R. Halmos, Naive Set Theory, Springer,1960Google Scholar
  9. 9.
    A.G. Hamilton, Logic for Mathematicians,(Revised Edn), Cambridge University Press,1988Google Scholar
  10. 10.
    J. Harrison,‘Formalized Mathematics,’ Math.Universalis, 2,1996,
  11. 11.
    M. Jackson, H. Lowe,“XBarnacle:Making Theorem Provers More Accessible,’ CADE-17, p502–506, LNAI 1831, Springer, 2000Google Scholar
  12. 12.
    L. Lamport,‘How to write a proof’, American Mathematical Monthly, 102(7): 600–608, 1994Google Scholar
  13. 13.
    U. Leron,‘Structuring Mathematical Proofs,’ American Mathematical Monthly 90(3):174–185,1983MathSciNetCrossRefGoogle Scholar
  14. 14.
    J. Nielsen, Usability Engineering, Morgan Kaufmann,1993Google Scholar
  15. 15.
    L.C. Paulson & K. Grabczewski,‘Mechanizing Set Theory,” Journal of Automated Reasoning, 17: 291–323, 1996MathSciNetCrossRefGoogle Scholar
  16. 16.
    G. Polya, How to Solve It, Penguin Books,1990Google Scholar
  17. 17.
    W. Rudin, Functional Analysis (2nd Edn), McGraw-Hill, 1991Google Scholar
  18. 18.
    J. Siekmann, S. Hess, C. Benzmüller, L. Cheikhrouhou, H. Horacek, M. Kohlhase, K. Konrad, A. Meier, E. Melis, M. Pollet, V. Sorge,‘LΩUI:Lovely Omega User Interface,’ Formal Aspects of Computing 11(3):1–17, 1999CrossRefGoogle Scholar
  19. 19.
    A. Strauss, J. Corbin, Basics of Qualitative Research:Techniques and Procedures for Developing a Grounded Theory, Sage Publications,1998Google Scholar
  20. 21.
    F. Wiedijk,The De Bruijn Factor,

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Authors and Affiliations

  • Paul Cairns
    • 1
  • Jeremy Gow
    • 1
  1. 1.UCL Interaction CentreUniversity College LondonLondonUK

Personalised recommendations