Lucas DixonTeaching → Project: A Proof Centric Proof Assistant

MSc Project Proposal: A Proof Centric Proof Assistant

Possible supervisors: Lucas Dixon, Jacques Fleuriot, David Aspinall

Principal goal of the project:

To develop a novel way of interacting with a proof planner based on the proof centric interface suggested by Dixon and Fleuriot's [3]. This will focus on providing way to explore the search space while preserving a structured view of the underlying proof plan.

Background:

Exciting developments in proof assistants have opened new ways to specify and develop systems and formalise mathematics. In particular, human-readable, declarative, but still machine checkable styles of writing proofs have recently been developed for higher order interactive proof assistants.

One example is the Isar [1] language which is the main used for interacting with the Isabelle proof assistant [2]. However, the syntax and the semantics of these language can be difficult to understand, even though they are relatively easy to read. New users find it difficult to know which commands can be written where, and even experienced users have difficulty predicting when and what the proof tactics will do.

Dixon and Fleuriot suggested that a proof assistant should focus interaction based around the construction of these readable and machine checkable proof [3]. They propose that an interface should work on incrementally constructing the proofs and allowing the user to explore their construction. This removes the burden from the user of understanding the semantics of Isar and the behaviour of the powerful proof tools.

Project Details:

This project is to develop a new interface, based on Texmacs [4], roughly following the proposal of Dixon and Fleuriot [3]. Namely that the exploring the development of an Isar-like proof script should be given machine support.

The IsaPlanner proof planner [5] will provide an internal language for the proofs. An interface will be built using the the TeXmacs system, a novel WYSWYG structured editor. The goal is to allow the sophisticated interaction and construction of proof scripts in an exploratory manner. The current interface for these systems is Proof General [6] which also defines a protocol for interaction. A secondary goal of this project is to suggest ways that the proof general protocol might be extended to support new ways to manipulate proof scripts.

The project is ambitious, leading to new research on interfaces for theorem provers, but is based on a strong software platforms. An initial interface will developed based on existing tools for interaction with IsaPlanner. Once this is completed, more complex interactions, as suggested in Dixon and Fleuriot, can be attempted. An evaluation can either be based on a case study by formalising some mathematics or by user-experiments.

Requirements:

Knowledge of scheme and ML are beneficial. It is strongly suggested that the student have taken the automated reasoning course and essential that they have some experience in functional programming.

Degree of Difficulty:

Challenging. It will require significant programming and creative insights into working with a proof planner. If a case formal study is attempted then some background in automated reasoning would also be important.

References: