imported>Son |
imported>Son |
| Line 1: |
Line 1: |
| − | == Introduction ==
| + | The Proof Manager is responsible for constructing proofs and maintaining existing proofs associated with proof obligations. |
| | | | |
| − | This document does NOT provide a way to avoid doing interactive proofs or pointing out the weakness of existing provers. Rather this document shows how to use information from doing interactive proofs to improve the clarity of models. As a consequence of these improvement, more obligations can be discharged automatically. We call these added information to the model "proof hints".
| + | For this, the Proof Manager architecture is separated into two parts: ''extensible'' part and ''static'' part. The extensible part is responsible for generating individual proof rules. The static part is responsible for putting proof rules together to construct and manage proofs. We call components that generate valid proof rules reasoners. |
| | | | |
| − | This concept of "proof hints" already exists in the form of "witness" or "theorem" in Event-B. These useful features are designed not only to help with proving the correctness of the model but also to give more information about the particular model.
| + | The basic reasoning capabilities of the Proof Manager can be extended by adding new reasoners. A reasoner may implement a decision procedure for automated proof, or a derived rule schema for interactive proof. |
| | | | |
| − | The question is how we can decide which "features" are useful to have in the model. In principle we can go to the extreme and include the whole proof strategy into the model in order to be able to have it being discharged automatically. But this is undesirable since it will make the model difficult to understand. Having taken this into account we specify our criteria here for "proof hints".
| + | == Reasoners == |
| | + | Reasoners are responsible for generating proof rules. The input of a reasoner is: |
| | | | |
| − | 1. It should help to understand the model better. | + | 1. A sequent. |
| | | | |
| − | 2. It should improve the automatic proving rate of the model. | + | 2. Optional input (e.g. a predicate in the case of the Cut Rule). |
| | | | |
| − | In fact, we regard the first criterion as more important whereas the second criterion can be considered as a bonus for improving the clarity of the model. Below are our proposal for two kinds of proof hints: [[Hypothesis Selection | hypothesis selection]] and proof by cases.
| + | The output of the reasoner (in case of successful) is a proof rule. This proof rule is ''trusted'' by the Proof Manager to built the proof. |
| | | | |
| − | == Proof Hints ==
| + | An important point about reasoners is that the internal workings of them are not visible to the other part of the Proof Manager. It is only required that they satisfy the following requirements: |
| | | | |
| − | The presentation for each kind of proof hints is as follows:
| + | a. '''Logically Valid''' A generated proof rule must be valid (i.e. can be derived) in the mathematical logic. |
| | | | |
| − | 1. '''Description''': A brief description of the proof hints with the situation where this can be helpful.
| + | b. '''Replayable''' A reasoner must work ''deterministically'', i.e. given the same input, a reasoner must generate the same proof rule every time. |
| | | | |
| − | 2. '''Example''': an example in Event-B is presented.
| + | == Maintaining Existing Proofs == |
| − | | |
| − | 3. '''Work around''': we show a solution (rather a work-around) for the current RODIN Platform.
| |
| − | | |
| − | === Hypothesis Selection === | |
| − | '''Description''' In order to discharge the proof obligation, the developer just selects some hypotheses then invoke either AtelierB P0 or newPP restricted to finish these proofs. The solution is to (somehow) give "hints" to the Proof Obligation Generator (POG) to select these hypotheses automatically when generating the corresponding proof obligation.
| |
| − | | |
| − | '''Example''' Consider the following Event-B model
| |
| − | | |
| − | [[Image:var-hypsel.png]] [[Image:inv-hypsel.png]]
| |
| − | | |
| − | [[Image:init-hypsel.png]] [[Image:set-hypsel.png]]
| |
| − | | |
| − | Consider the proof obligation '''set/hypSel0_1/INV''' which states that the event '''set''' maintains invariant '''hypSel0_1''' (Here <math>\ldots</math> denotes the unselected hypotheses).
| |
| − | [[Image:set-hypSel0_1-INV.png]]
| |
| − | | |
| − | Any provers works with only the selected hypotheses cannot discharge the above proof olbligation since the hypothesis <math>x \neq 0 \limp y \in \nat</math> is missing. The obligation with the appropriate hypothesis selection is as follows
| |
| − | [[Image:set-hypSel0_1-INV-sel.png]]
| |
| − | | |
| − | '''Workaround''' Currently, given and event '''evt''' and invariant '''inv''', the invariant preservation proof obligation '''evt/inv/INV''' generated with the following hypotheses automatically selected;
| |
| − | | |
| − | * The invariant '''inv'''
| |
| − | | |
| − | * The guard of the event '''evt'''
| |
| − | | |
| − | In order to have the needed hypothesis selected automatically, we will add this hypothesis into the guard. Moreover, in order to avoid changing event's behaviour, we will mark this extra guard as a theorem. Apply this technique, the new event '''set''' is as follows
| |
| − | [[Image:new-set-hypsel.png]]
| |
| − | | |
| − | Note that the extra (theorem) guard can be removed in the further refinement without generating any new proof obligation.
| |
| − | | |
| − | === Case distinction ===
| |
| − | '''Description''' In order to discharge a proof obligation, the developer makes a manual "proof by cases" based on some condition <math>P</math>. Afterwards, all branches of the proofs are discharged either by ML or AtelierB P0. The solution is to (somehow) give "hints" to the POG to generate different proof obligations for each case separately. ''Proof by cases'' is usually not applied automatically since this splits the proof tree which could lead to blows up in terms of the number of cases.
| |
| − | | |
| − | '''Example''' Consider the following Event-B model
| |
| − | | |
| − | [[Image:casesplit.png]]
| |
| − | | |
| − | Consider the proof obligation '''set/case0_1/INV''' (Here all hypotheses, including those hidden are shown)
| |
| − | | |
| − | [[Image:set-case0_1-INV.png]]
| |
| − | | |
| − | In order to finish the proof, a correct "proof by cases" is done to consider <math>a = 1</math> or <math>a \neq 1</math>.
| |
| − | | |
| − | '''Workaround''' To capture the effect of doing '''proof by cases''', we split the original event '''set''' into two different events as follows
| |
| − | | |
| − | [[Image:new-set-evts.png]]
| |
| − | | |
| − | In the next refinement step, we can merge the above two new event to the original event as follows.
| |
| − | | |
| − | [[Image:merged-set.png]]
| |
| − | | |
| − | [[Category:Proof]]
| |
| − | [[Category:Work in progress]]
| |
The Proof Manager is responsible for constructing proofs and maintaining existing proofs associated with proof obligations.
For this, the Proof Manager architecture is separated into two parts: extensible part and static part. The extensible part is responsible for generating individual proof rules. The static part is responsible for putting proof rules together to construct and manage proofs. We call components that generate valid proof rules reasoners.
The basic reasoning capabilities of the Proof Manager can be extended by adding new reasoners. A reasoner may implement a decision procedure for automated proof, or a derived rule schema for interactive proof.
Reasoners
Reasoners are responsible for generating proof rules. The input of a reasoner is:
1. A sequent.
2. Optional input (e.g. a predicate in the case of the Cut Rule).
The output of the reasoner (in case of successful) is a proof rule. This proof rule is trusted by the Proof Manager to built the proof.
An important point about reasoners is that the internal workings of them are not visible to the other part of the Proof Manager. It is only required that they satisfy the following requirements:
a. Logically Valid A generated proof rule must be valid (i.e. can be derived) in the mathematical logic.
b. Replayable A reasoner must work deterministically, i.e. given the same input, a reasoner must generate the same proof rule every time.
Maintaining Existing Proofs
