Difference between pages "Rodin Platform 2.0 Release Notes" and "Rodin Proving Perspective"
From Event-B
(Difference between pages)
Jump to navigationJump to searchimported>Tommy m (→Requirements) |
imported>Im06r |
||
Line 1: | Line 1: | ||
+ | {{Navigation|Previous= [[The_Proof_Obligation_Explorer_(Rodin_User_Manual)|The Proof Obligation Explorer]]|Next= [[The_Mathematical_Language_(Rodin_User_Manual)|The Mathematical Language]]|Up= [[index_(Rodin_User_Manual)|User_Manual_index]]}} | ||
{{TOCright}} | {{TOCright}} | ||
+ | == Overview == | ||
+ | The Proving Perspective is made of a number of windows (views): the Proof Tree, the Goal, the Selected Hypotheses, the Proof Control, the Proof Information, and the Search Hypotheses. In subsequent sections, we study each of these windows. Below is a screenshot of the proving perspective: | ||
− | == | + | == 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 12:26, 11 March 2010
Contents |
Overview
The Proving Perspective is made of a number of windows (views): the Proof Tree, the Goal, the Selected Hypotheses, the Proof Control, the Proof Information, and the Search Hypotheses. In subsequent sections, we study each of these windows. Below is a screenshot of the proving perspective:
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.