Papers at UITP'97

• Providing Relevant Feedback by Critiquing
  J. S. Aitken and P. Gray
• An Environment for Integrating Formal Methods Tools
  P. Anderson, M. Goldsmith, B. Scattergood, and T. Teitelbaum
• Direct manipulation of Algebraic Formulae in Interactive Proof Systems
  Y. Bertot
  [dvi format] (34k) , [gzipped postscript format](78k), related work.
• Algebraic Semiotics, ProofWebs and Distributed Cooperative Proving
  J. Goguen, A. Mori, and K. Lin
  [gzipped postscript format], related work.
• The Minimal User-Interface of a Simple Refinement Tool
  P. Heuberger
  [dvi format], [postscript format], related work.
• Cognitive Dimensions Analysis of Theorem Provers
  G. .F. Kadoda and R. Stone
• Evaluation of a Semi-Automated Theorem Prover (Part I)
  H. Lowe
• Evaluation of a Semi-Automated Theorem Prover (Part II)
  M. J. Jackson
  [gzipped postscript format] (48k)
• What is Wrong with GUIs for Theorem Provers
  N. A. Merriam and M. D. Harrison
  [dvi format](33k), [gzipped postscript](110k), related work.
• Directing Proofs by Documenting and Pointing: CafeOBJ on Network
  A. T. Nakagawa and A. Seo
• Undoing and Managing a proof
  O. Pons
  [gzipped postscript format], related work.
• A User Interface for Controlling Term Rewriting Based on Computing-as-Editing Paragdigm
  Y. Takebe and M. Hagiya