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>