Proof Skeleton View: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Laurent
imported>Laurent
Line 1: Line 1:
==Purpose==
==Purpose==


The Proof Skeleton View allows to quickly browse through a proof build either automatically or interactively with the Rodin prover. This view can be used on any proof, independently of the presence of a corresponding proof obligation.
The Proof Skeleton View allows to quickly browse through a proof built either automatically or interactively with the Rodin prover. This view can be used on any proof, independently of the presence of a corresponding proof obligation.


Furthermore, this view allows user to see together proof rules and corresponding sequents.
Furthermore, this view allows user to see together proof rules and corresponding sequents.

Revision as of 13:58, 29 January 2009

Purpose

The Proof Skeleton View allows to quickly browse through a proof built either automatically or interactively with the Rodin prover. This view can be used on any proof, independently of the presence of a corresponding proof obligation.

Furthermore, this view allows user to see together proof rules and corresponding sequents.

The Proof Skeleton View

Showing the View

The Proof Skeleton View is available as other views in the Window > Show View > Other > Event-B > Proof Skeleton View menu.

To watch a proof skeleton, simply select a proved predicate in the obligation explorer, or a proof file in the editor.

View Interpretation

Proof skeletons are displayed in a two-part view. On the left hand side is the tree structure of rules applied in the proof. On the other side stands the sequent on which the currently selected rule is applied.

The tree can be expanded or collapsed by using [+] and [-] buttons on the upper right corner.