Next: Contents   Contents

---

• Contents
• List of Figures
• Introduction
• Background
  • Proof Checkers
  • Proof Generators
  • Proof Assistants
  • User Interfaces to Proof Assistants
    • Pcoq and CtCoq
    • Proof General
    • XEmacs Proof General
    • XIsabelle
    • DOVE
    • IsaWin
  
  
• Application Description
  • Task Analysis
  • Design Criteria
    • Usability
    • Functionality
  • Desirable Interaction Styles
    • Direct Manipulation
    • Menus and navigation
    • Command entry
  
  
• System Design
  • Language/Library Selection
  • Proof Assistant Selection
    • Proving in Isabelle
    • The future of Proof General
  • System Architecture
  • Communicator
  • Mediator
  • PGIP and PGML
  • Isabelle Server
  • GUI
  
  
• Proposed Amendments to PGIP
  • Library Management
  • Proof Steps
  
  
• Conclusion
  • Difficulties Overcome
  • State of Implementation
  • User Feedback
  • Further Work
    • PGIP Support
    • Other Proof Engines
    • Other Platforms
    • Equation Editor
  • Concluding Remarks
  
  
• Bibliography
• Sample Proof
  • Human-written
  • Proof using Igloo
  
  
• PGIP & PGML Schema
  • PGIP
  • PGML
  
  
• About this document ...

---

2003-11-08