Adding Manual Inference Reasoners

Beside the input sequent, reasoners of this type have two extra inputs specify the hypothesis or the goal and the position inside the predicate when apply an inference rule to the input sequent. As an example, consider the following inference rule (called IMP_R).

$\frac{H, P \vdash Q}{H \vdash P \limp Q}$

IMP_R

In this simple case the location is the location of the implication symbol in the goal.

Declare the Reasoner

• Create a new plug-in project, e.g. org.eventb.contributors.seqprover.implinference. Deselect the plug-in options for "Generating an activator" and "Contribution to the UI".

• Add dependency on the project org.eventb.core.seqprover

• Add an extension for org.eventb.core.seqprover.reasoners for our implication rewrite reasoner, e.g.

<extension point="org.eventb.core.seqprover.reasoners">
  <reasoner
    class="org.eventb.internal.contributors.seqprover.implinference.ManualInference"
    id="manualInference"
    name="%manualInferenceName"/>
</extension>

(add the key manualInferenceName to the plugin.properties accordingly).

• We will use Tom to implement the reasoner class itself.