Difference between revisions of "Rodin Proving Perspective"

From Event-B
Jump to navigationJump to search
imported>Im06r
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]]}}
 
{{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}}
 +
The Proving Perspective is made of a number of windows: the proof tree, the goal, the selected hypotheses, the proof control, the proof information, and the searched hypotheses. In subsequent sections, we study these windows, but before that let us see how one can load a proof.
  
 
== Loading a Proof ==
 
== Loading a Proof ==

Revision as of 17:14, 9 March 2010

The Proving Perspective is made of a number of windows: the proof tree, the goal, the selected hypotheses, the proof control, the proof information, and the searched hypotheses. In subsequent sections, we study these windows, but before that let us see how one can load 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 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.