D23 Improvements to Existing Provers

Overview

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

• 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 do proofs
• evolving 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 contributed 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

Proof storage in database ? TODO A more generical way to contribute tactics (New tactic provider API)

Available Documentation

The following pages give useful information about prover improvements:

• Prover Rules

See http://wiki.event-b.org/index.php/Inference_Rules

See http://wiki.event-b.org/index.php/All_Rewrite_Rules

• Proof Skeleton View

See http://wiki.event-b.org/index.php/Proof_Skeleton_View

• Proof Purger

See http://wiki.event-b.org/index.php/Proof_Purger_Interface

• Prover API evolution

See http://wiki.event-b.org/index.php/New_Tactic_Providers

• Versioned Reasoners

See http://wiki.event-b.org/index.php/Versioned_Reasoners

Planning

Proof storage in database ? TODO