Difference between revisions of "Adding Automatic Inference Reasoners"

From Event-B
Jump to navigationJump to search
imported>Son
(New page: Beside the input sequent, reasoners of this type does not have any extra input and automatically applies an inference rule to the input sequent. As an example, consider the following infer...)
 
imported>Son
Line 19: Line 19:
 
(add the key autoInferenceName to the plugin.properties accordingly).
 
(add the key autoInferenceName to the plugin.properties accordingly).
  
−
* Click on the class attribute of the newly created extension. A dialog appears for new class wizard.
+
* We will use Tom to implement the reasoner class itself.
  
−
* The abstract implementation of this class is ''org.eventb.internal.core.seqprover.eventbExtensions.rewriters.AbstractAutoRewrites''. Choose this as the Superclass in the new class wizard. (For the moment, the class is internal within the project and subjected to be changed. Clients can make a copy of this class to develop their own implementation).
+
== Setting up Tom ==
−
 
 
−
* Finish the wizard and a new implementation for AutoRewrites class is created.
 
−
 
 
−
* The implementation can be as follows:
 

Revision as of 14:21, 15 September 2008

Beside the input sequent, reasoners of this type does not have any extra input and automatically applies 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

Create 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.AutoInference"
    id="autoInference"
    name="%autoInferenceName"/>
</extension>

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

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

Setting up Tom

Retrieved from ‘https://wiki.event-b.org/index.php?title=Adding_Automatic_Inference_Reasoners&oldid=586’