Project: A Proof General for 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:

• Writing a simple parser for the Proof Plan language.
• Providing a interface for working with the plans in the new Eclpise/PGIP based version of Proof General.
• Providing IsaPlanner with the appropriate PGIP commands to talk to Proof General.

To evaluate the project, a small case study will be performed. This will examine how easily the plans can be generated interactively and be compared to writing Isar proof scripts as well as automatically generated plans.

Background in Automated Reasoning and Interfaces would be beneficial, but not essential. Experience with writing compilers would also be very helpful.
The project will involve writing Java and ML code, so knowledge of these languages would also be helpful.

• Proof General
• IsaPlanner
• Eclipse