Extending the Proof Manager

The Proof Manager is responsible for constructing proofs and maintaining existing proofs associated with proof obligations.

There are two ways for extending the Proof Manager:

1. adding a new reasoner.

1. adding a new tactic.

Adding a New Reasoner

A reasoner is added into the Proof Manager using the extension point org.eventb.core.seqprover.reasoners. Below are 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>

where the name attribute is internationalized.

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 class attribute must be a valid Java class name which will be used to create an instance of the reasoner. This class must implements org.eventb.core.seqprover.IReasoner interface.