Sequent Prover

Using ProB, sequents can be proven interactively. For the construction of a formal proof, rules for rewriting expressions or decomposing proof goals into simpler subgoals are applied. To discharge a proof obligation one has to prove one or more sequents, consisting of hypotheses and a goal that must be derived from the hypotheses.

Currently, .pl files with proof obligations can be loaded which are exported from Rodin. To generate these files, an Event-B component must be selected in Rodin and the option ProB Standalone > Export POs for ProB must be invoked.

All rules that are applicable to the current sequent are displayed in the Operations View. The implemented rules include the inference and rewrite rules available in Rodin:

• https://wiki.event-b.org/index.php/Inference_Rules
• https://wiki.event-b.org/index.php/All_Rewrite_Rules

The State View shows the current sequent, including its hypotheses and goal, as well as important state properties. Furthermore, the State Visualisation presents both the current state and the preceding state, allowing a comparison between consecutive steps. By right-clicking on a predicate within this visualisation, the user can see rules that are applicable to that selected element.

(Overview img)

Transitions

Some rules require additional user input, i.e. an expression or a predicate. This is necessary, for example when it is necessary to add a new hypothesis to advance the proof, to instantiate quantifiers like the existential quantifier or perform a case distinction.

Transitions for these rules are displayed in orange / with a question mark. This indicates that the subsequent state is not computed in advance, either because the execution depends on user input, so they cannot be precomputed or it is a transition for an external provers (where no parameters are expected).

skip_to_cont is a transition that allows you to skip the current sequent and prove it later. If it is selected here, arr ∈ ℤ ⇸ ℤ will be the next goal. CONTINUATION denotes the number of additional sequents in the proof, so now there are four sequents in total, including the current sequent.

Input Syntax

User input has to be provided in B Syntax. Due to syntactic differences between B and Event-B, certain operators must be adapted accordingly. For instance, a cartesian product is written as S ** T, exponentiation as a^b and set difference as S \\ T (note that it is written as \\ in the input because of the escape character \). finite(S) is an Event-B operator and is entered as S:FIN(S).

To illustrate a valid input, this is an example predicate for a hypothesis to be added (x ≠ 0 ∧ s ∪ t ⊂ ℕ):

Saving Proofs

To save a proof, the proof trace can be stored as a .prob2trace file (1a), which can later be reloaded and reused (1b). This option allows proofs to be revised, for example by interactively replaying the trace and modifying some steps. Alternatively, proofs can be exported as HTML documents (2):

Automatic Provers

In addition to interactive proving, ProB allows the invocation of external automatic provers. This can be useful for determining whether a given sequent is provable at all. The following provers can be called:

• the ProB (Dis-)Prover which searches for counterexamples and can invalidate and prove sequents
• ProB's well-definedness prover for discharging well-definedness proof obligations
• Atelier B's mono-lemma (ml) prover and predicate prover (pp)

To use the Atelier B provers, the path to the krt tool must be set via File > Preferences > ATELIERB_KRT_PATH. If the provers from Atelier B were installed in Rodin, the krt executable might be found within Rodin's configuration directory (path is possibly /Users/.../rodin/configuration/org.eclipse.osgi/.../krt).

The question mark shown on transitions for external provers also indicates that they may not be executable. It is the case if too many or unsuitable hypotheses are selected for proving the goal.