Lucas Dixon →
Teaching →
Project: A Proof General for Proof Plans

To develop a Proof General mode for editing IsaPlanner's Proof Plans.

Supervisors: David Aspinall, Lucas Dixon

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.

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.