Sequent Prover Developer Guide

Programmer's Guide

Welcome to Event-B Sequent Prover

The Event-B sequent prover is a plug-in for the Eclipse platform which provides different proof rules to be used within the Rodin Tool. The following sections discuss the issues when extending the Event-B sequent prover.

Sequent Prover Core

Sequents

TODO

Proof Rules

TODO

Proof Trees

TODO

Reasoners

Concepts

Reasoners are used in the Event-B sequent prover to generate proof rules. A reasoner is provided with the sequent to prove as well as some extra optional input. The reasoner is implemented by a computer program and it is the job of the developers to ensure that the reasoners either fail or generate logically valid proof rules.

An example of a reasoner is the "conjI" reasoner that generates the conjI proof rules, which splits a conjunctive goal into two sub-goals. Here, assume that the input sequent is $A, B, C \vdash D \land E$, the conjI reasoner produces the following proof rules.

$\frac{\quad A, B, C \vdash D ~~~ A, B, C \vdash E\quad}{A, B, C \vdash D \land E}$

Adding a reasoner

A reasoner is added into the Event-B sequent prover using the extension point org.eventb.core.seqprover.reasoners. Below is an example of how to contribute to the extension point.

<extension point="org.eventb.core.seqprover.reasoners">
  <reasoner
     class="org.eventb.contributors.seqprover.reasoners.Hyp"
     id="hyp"
     name="%hypName"/>
</extension>

The above declaration defines a reasoner with a specific id (which will be automatically prefixed by the project name, e.g. org.eventb.contributors.seqprover). The name is an externalised string which is used for display purpose.

The class attribute must be a valid Java class name which will be used to create an instance of the reasoner. This class must implement the org.eventb.core.seqprover.IReasoner interface.

However, most of the time, developers only need to extend one of the abstract implementation (depending on the type of the reasoner). For this implementation purpose, the type of the reasoners are specified below:

1. Automatic rewriting reasoners: Reasoners which apply some rewriting rules automatically to simplify the sequent.
2. Automatic inference reasoners: Reasoners which apply an inference rule automatically.
3. Manual rewriters: Reasoners which apply a rewriting rule at a given position.
4. Manual inference: Reasoner which apply an inference rule manually.
5. General reasoners: If the reasoner does not fall into the above categories, clients need to implement the interface IReasoner directly.

Implementing a reasoner is only a first step of contributing to the sequent prover. In order to use a reasoner, the reasoner needs to be wrapped around by a tactic.