Difference between revisions of "Extending the Proof Manager"

From Event-B
Jump to navigationJump to search
imported>Son
imported>Son
Line 31: Line 31:
 
* [[Adding Manual Rewrite Reasoners | Manual rewrite]] Reasoners of this type apply a rewriting rule for a given formula (or sub-formula) in the goal or in one of the hypotheses.
 
* [[Adding Manual Rewrite Reasoners | Manual rewrite]] Reasoners of this type apply a rewriting rule for a given formula (or sub-formula) in the goal or in one of the hypotheses.
  
* [[Extending the Proof Manager#Automatic Inference Reasoners|Automatic inference]] Reasoners of this type apply an inference rule automatically.
+
* [[Adding Automatic Inference Reasoners | Automatic inference]] Reasoners of this type apply an inference rule automatically.
  
 
* [[Extending the Proof Manager#Manual Inference Reasoners|Manual inference]] Reasoner of this type apply and inference rule manually.
 
* [[Extending the Proof Manager#Manual Inference Reasoners|Manual inference]] Reasoner of this type apply and inference rule manually.
  
 
* [[Extending the Proof Manager#General Purpose Reasoners|General purpose]] Reasoners that do not fall into the four previous categories.
 
* [[Extending the Proof Manager#General Purpose Reasoners|General purpose]] Reasoners that do not fall into the four previous categories.
 
=== Automatic Inference Reasoners ===
 
  
 
=== Manual Inference Reasoners ===
 
=== Manual Inference Reasoners ===

Revision as of 13:52, 15 September 2008

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 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>

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.

However, most of the time, the developers only need to sub-class one of the abstract implementation, depending on the type of the reasoner. For the implementation purpose, we categorize our reasoners into the following types.

  • Automatic rewrite Reasoners of this type apply some rewriting rules automatically to simplify the input sequent.
  • Manual rewrite Reasoners of this type apply a rewriting rule for a given formula (or sub-formula) in the goal or in one of the hypotheses.
  • General purpose Reasoners that do not fall into the four previous categories.

Manual Inference Reasoners

General Purpose Reasoners

Adding a New Tactic