Rodin Proving Perspective: Difference between revisions
From Event-B
Jump to navigationJump to search
imported>Im06r No edit summary |
imported>Im06r |
||
| Line 3: | Line 3: | ||
== Loading a Proof == | == Loading a Proof == | ||
In order to load a proof, enter the Proof Obligation window, select the project, select and expand the component, finally select the proof obligation: the corresponding proof will be loaded. As a consequence: | |||
* the proof tree is loaded in the Proof Tree window. As we shall see in section [[The_Proving_Perspective_(Rodin_User_Manual)#The_Proof_Tree|6.2]], each node of the proof tree is associated with a sequent. | |||
* In case the proof tree has some "pending" nodes (whose sequents are not discharged yet) then the sequent corresponding to the first pending node is decomposed: its goal is loaded in the Goal window (section [[The_Proving_Perspective_(Rodin_User_Manual)#Goal and Selected Hypotheses|6.3]]), whereas parts of its hypotheses (the "selected" ones) are loaded in the Selected Hypotheses window (section [[The_Proving_Perspective_(Rodin_User_Manual)#Goal and Selected Hypotheses|6.3]]). | |||
* In case the proof tree has no pending node, then the sequent of the root node is loaded as explained previously. | |||
Revision as of 17:06, 9 March 2010
Loading a Proof
In order to load a proof, enter the Proof Obligation window, select the project, select and expand the component, finally select the proof obligation: the corresponding proof will be loaded. As a consequence:
- the proof tree is loaded in the Proof Tree window. As we shall see in section 6.2, each node of the proof tree is associated with a sequent.
- In case the proof tree has some "pending" nodes (whose sequents are not discharged yet) then the sequent corresponding to the first pending node is decomposed: its goal is loaded in the Goal window (section 6.3), whereas parts of its hypotheses (the "selected" ones) are loaded in the Selected Hypotheses window (section 6.3).
- In case the proof tree has no pending node, then the sequent of the root node is loaded as explained previously.
