To develop a Proof General mode for editing IsaPlanner's Proof Plans.
Proof Plans provide a hierarchical representation for proofs. This
structure offers new and interesting ways to interactively
derive proofs. This project aims to build on IsaPlanner, a proof
planner which provides a concrete representation of proof plans, and
Proof General, which emboies a methodology for interacting with proof
systems. The aim is to develop a Proof General mode for working with
the proof plans of IsaPlanner.
A Basic implementation will involve a parser for the Plan language, which will be similar to the Isar parser, and a basic proof general mode that allows the user to type in parts of the plan. The Proof General interface will send the appropriate commands to IsaPlanner to check that the plan is well formed. This is much the same architecture as other existing modes for Proof General. However, the hierarchical nature of the plans allows the interface to be extended by implementing a menu-driven approach to writing the plans, and by allowign techniques in IsaPlanner to automatically generate parts of the plan. In particular, this project will involve:
Background in Automated Reasoning and Interfaces would be beneficial,
but not essential. Experience with writing compilers would also be
The project will involve writing Java and ML code, so knowledge of these languages would also be helpful.