Overview
The project concerns the development of a system for presenting and
manipulating hierarchical proofs and graphs as generated by proof
planning in IsaPlanner.
Grant Information
This is funded by "The Integration and Interaction of Multiple Mathematical Reasoning Processes"
EPSRC Platform Grant GR/S01771/01.
Download/Installation/Setup
From subversion with the command:
svn co https://isaplanner.svn.sourceforge.net/svnroot/isaplanner/trunk/HiGraph HiGraph
This is a Java1.5 program. The project includes eclipse project configuration, so the easiest way to run it is to use eclipse to build it, and run it as a java application with there.
Developers
Lucas Dixon, Alex Redstone and Graham Dutton.
Relevant Research Papers and Talks
Tutorial
A brief introduction to the HiProof interface is available here.
Bugfixes and improvements needed:
- Fixed ordering (user modifiable) on subgoals for consistent presentation
- Preferences saved to file and applied to individual HiGraphs, or globally across the application
Forthcoming features:
- Interface with IsaPlanner
- Mathematical symbols in names (possibly using MathML)
- Drag-and-drop interface
- Goals in a submethod should be able to leave their containing method to become a child-method.
- Methods with multiple incoming goals
Current Features
- Users can interactively edit graphs
- Cut/Copy/Paste actions available to speed up editing
- Preferences such as colours, line widths and fonts are user-definable
- HiGraphs are loaded from or saved to a XML format
- Navigation of HiGraphs aided by 3-level zooming which gives local context in proof
