imported>Nicolas |
|
| Line 1: |
Line 1: |
| − | = 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 http://wiki.event-b.org/index.php/Inference_Rules]
| |
| − | : See [http://wiki.event-b.org/index.php/All_Rewrite_Rules http://wiki.event-b.org/index.php/All_Rewrite_Rules]
| |
| − | * Proof Skeleton View
| |
| − | : See [http://wiki.event-b.org/index.php/Proof_Skeleton_View http://wiki.event-b.org/index.php/Proof_Skeleton_View]
| |
| − | * Proof Purger
| |
| − | : See [http://wiki.event-b.org/index.php/Proof_Purger_Interface http://wiki.event-b.org/index.php/Proof_Purger_Interface]
| |
| − | * Prover API evolution
| |
| − | : See [http://wiki.event-b.org/index.php/New_Tactic_Providers http://wiki.event-b.org/index.php/New_Tactic_Providers]
| |
| − | * Versioned Reasoners
| |
| − | : See [http://wiki.event-b.org/index.php/Versioned_Reasoners http://wiki.event-b.org/index.php/Versioned_Reasoners]
| |
| − |
| |
| − |
| |
| − | = Planning =
| |
| − |
| |
| − | Proof storage in database ? {{TODO}}
| |
| − |
| |
| − |
| |
| − | [[Category:D23 Deliverable]]
| |
