Overview

All along the lifecycle of the provers, the following improvements can be achieved by:

Adding new useful proof rules (to prove sequents that are hard to prove or even not provable at all).
Correcting bugs in implementations of existing proof rules.
Implementing new tools to help the user to do proofs.
Evolving the prover API to fit with the needs of prover plug-in developers.

Part of implemented rules and user interface features come from user feedback, mainly through SourceForge feature requests. SourceForge bugs are also an important source of input for corrections.

Systerel is in charge of existing prover improvements. University of Southampton gave feedback for the definition of prover API evolution.

Motivations

Areas of improvement for provers can be summarized as follows:

Reducing proving time and effort.

New proof rules.

Reflecting prover implementation corrections.

Reasoner versioning.

Reducing proof storage space.

Proof purging.

Proof simplifying.

Non textual database storage.

Facilitating manual proof review or reuse.

Proof skeleton view.

Copy / paste from skeleton to edited proof.

Prover API evolution.

New tactic provider API.

Choices / Decisions

A problem showed up while trying to implement a new proof rule (substitution of the domain of a total function). It required to make a reasoner able to propose several substitutions for the same function. More generally, the problem was to parameterize how a given rule shall be applied, depending on a user choice among various possible applications. Each choice should be displayed in the popup list in interactive proving. Before the improvement, a given reasoner could only propose one application. Thus, we had to define a new, more general, API. At the same time, the University of Southampton was working on Rule-Based Provers and they were also meeting difficulties dealing with the old API. We then started a discussion in order to define a new API that would address everyone's needs. Proposals were made on a wiki page (http://wiki.event-b.org/index.php/New_Tactic_Providers) until it reached a stable state.

During Deploy plenary meeting (October 2009), the idea arose to change proof storage means in order to enlighten proof files, which can grow very large with current XML Rodin database storage. Possible solutions are to be investigated.