Difference between pages "Adding Reasoners(How to extend Rodin Tutorial)" and "Theory Release History"

From Event-B
(Difference between pages)
Jump to navigationJump to search
(Antecedent and needed hypotheses were mixed up)
 
(Theory plug-in release 4.0.3)
 
Line 1: Line 1:
−
{{Navigation|Previous= [[Extending_the_Proof_Obligation_Generator(How_to_extend_Rodin_Tutorial) | Generating the proof obligations]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]]}}
+
Back to [[Theory Plug-in]].
  
−
=== Principles ===
+
Follow this page for the latest on the Theory plug-in. The user manual is also provided together with the installation details.
−
Rodin support several provers. Some are embedded such as NewPP, or the sequent prover which will talk about here, and some are added by external plug-ins (as the Atelier B provers : ML, PP, P0, etc).
 
  
−
Contributing to Rodin sequent prover is done by adding tactics. These tactics which often involve a set of reasoners, apply on proof tree nodes. The reasoners apply on the sequent of a given proof tree node. A reasoner is (and has to be) quite "rough" : it shall take a given sequent and produce a proof rule that will (if possible) apply on this given sequent, whereas a tactic could be smarter. Indeed, a tactic can involve several reasoners, thus apply them in loops, and combine them, or even call other tactics. A tactic can be either automatic (auto tactic and/or post tactic) or manual (using providers in the UI that paint their applications in red on formulas) in case of interactive proof.<br>
+
===News===
 +
* ''29th September 2021'': [[#Version_4.0.3|Version 4.0.3]] is released. It requires Rodin 3.5.
 +
* ''4th June 2021'': [[#Version_4.0.2|Version 4.0.2]] is released. It requires Rodin 3.5.
 +
* ''22th December 2020'': [[#Version_4.0.1|Version 4.0.1]] is released. It requires Rodin 3.5.
 +
* ''19th December 2014'': [[#Version_3.0.0|Version 3.0.o]] is released. It requires Rodin 3.1.
 +
* ''10th July 2014'': [[#Version_2.0.2|Version 2.0.2]] is released. It requires Rodin 2.8.
 +
* ''24th June 2014'': [[#Version_2.0.1|Version 2.0.1]] is released. It requires Rodin 2.8.
 +
* ''30th April 2014'': [[#Version_2.0.0|Version 2.0.0]] is released. It requires Rodin 2.8. This release contains major changes in the features and accessibilities.
 +
* ''20th April 2012'': [[#Version_1.3.2|Version 1.3.2]] is released. It requires Rodin 2.4.
 +
* ''15th August 2011'': [[#Version_1.2|Version 1.2]] is released. It requires Rodin 2.2.2.
 +
* ''6th August 2011'': [[#Version_1.1|Version 1.1]] is released. It requires Rodin 2.2.2.
 +
* ''8th July 2011'': [[#Version_1.0|Version 1.0]] is released. It requires Rodin 2.2.
 +
* ''22nd May 2011'': [[#Version_0.8|Version 0.8]] released. It is based on Rodin 2.1.1.
 +
* ''11th April 2011'': [[#Version_0.7|Version 0.7]] released. It is based on Rodin 2.1.1.
 +
* ''6th January 2011'': [[#Version_0.6|Version 0.6]] released. It is based on Rodin 2.0.1.
 +
* ''28th October 2010'': [[#Version_0.5|Version 0.5]] released. It is based on Rodin 2.0.
  
−
[[Image:Adding_Reasoners_TacticsImage.png|400px|center]]
+
===Releases===
 +
===== Version 4.0.3 =====
 +
''29th September 2021''
  
−
A reasoner encapsulates a kind of "proof step", also called "proof rule". The sequent prover provides a set of tactics applying proof rules (and even other tactics!). These rules are either rewriting rules (see [[All_Rewrite_Rules|rewriting rule list]]) or inference rules (see [[Inference_Rules|inference rule list]]). It is actually a really critical piece of code, that developers should understand at first sight, and be convinced about its correctness. If one codes a wrong reasoner, one breaks the whole soundness of proofs done within Rodin! As they are written in pure java, and accorded to the previous considerations, they have to be the simpliest and most readable as possible. Finally, it is needed to write tests that cover all the possible cases of application of one given reasoner (this will not be detailed in this tutorial).
+
Release target: Rodin 3.5
 +
* Bug fixes:
 +
** Operators that have parameters with the same name but different types are now handled correctly in both the editor and the prover (for rewriting the definition)
 +
** Theorems instantiated during proof are now correctly typed (in some cases, some type information was missing)
  
−
=== In this part ===
+
===== Version 4.0.2 =====
−
In this part we will see how to contribute to the sequent prover of Rodin by encapsulating a new proof rule within a reasoner and add a tactic to the sequent prover of Rodin that will encapsulate this reasoner.
+
''4th June 2021''
−
The rule, coded within the reasoner, that we want to apply is the following:
 
  
−
{| cellpadding="20" cellspacing="0" border="1"
+
Release target: Rodin 3.5
−
|<math>\frac{ \textbf{H},\; a = b \;\; \vdash \;\; \textbf{G}} {\textbf{H},\; a \leq b,\;b \leq a\;\vdash \;\; \textbf{G}}</math>
+
* Bug fixes:
−
| DBL_INEQ
+
** Datatypes that have several type parameters are now serialized in the right order; it fixes some issues with proofs and proof replay.
−
|}
+
** Manually applied inference and rewrite rules are now replayed correctly (in some cases, their replay was displayed as uncertain).
  
−
Let's call this rule DBL_INEQ. By reading this rule, we see it is goal agnostic. This means that the rule will be applied if the prover sequent under consideration contains the hypotheses <math>a \leq b,\;b \leq a</math>, whatever the goal of this sequent. We will say that <math>a \leq b,\;b \leq a</math> are the "Needed hypotheses".
+
===== Version 4.0.1 =====
 +
''22th December 2020''
  
−
[[Image:Adding_Reasoners_DBL_INEQ_Reasoner.png|550px|center]]
+
Release target: Rodin 3.5
 +
* Bug fixes:
 +
** The theory plugin now takes into account updates in theories, as well as creating a theory after using it (there was a cache issue).
 +
** The error messages at launch about rule-based provers failing to find the context of the proof have been removed.
 +
** The dropdown list in theory imports is now usable (there was an off-by-one issue when selecting an element in the list).
 +
** Manually applying an inference rule no longer throws a NullPointerException.
 +
** It is now possible to rename theories.
 +
** The TheoryPath creation dialog box has been simplified.
 +
* Optimizations:
 +
** The proving interface is now much more responsive, even when a theory contains a lot of rewrite rules (we have implemented a cache of the places where a rewrite rule can apply).
 +
** The theory plugin now generates much simpler WD conditions, especially for the pred, succ, prj1, prj2, and id operators.
  
−
Moreover, <math>\textbf{H}</math> is the set of selected hypotheses from the input sequent, and <math> a = b\;\vdash \;\textbf{G}</math> is the antecedent of the rule (i.e. a child node to be proved).
+
===== Version 4.0.0-RC1 =====
 +
''10th April 2017''
  
−
=== Step1 ===
+
Release target: Rodin 3.2
−
* Create a new plugin that will host our reasoner and tactic. It will not be any activator for this plug-in but the option "Activate this plug-in when one of its classes is loaded" shall be selected.
+
* AST Extensions (4.0.0) Major API change.
−
* Add a dependencies to the plug-ins <tt>org.eclipse.core.resources</tt>, <tt>org.eclipse.core.runtime</tt>, <tt>org.eclipse.ui</tt>, <tt>org.rodinp.core</tt>, <tt>org.eventb.core.ast</tt>,<tt>org.eventb.core.seqprover</tt> and <tt>org.eventb.core</tt>.
+
** Compatibility upgrade to Rodin 3.2
−
* Add the extension point <tt>org.eventb.core.seaqprover.reasoners</tt>, and create a 'reasoner' extension for our reasoner with ''"id : dblIneq"'' and ''"name :  Double Inequality"'' and finally,
+
** Support for get operator position for INFIX extended predicate operators.
−
* Create a new class for the reasoner, called <tt>DoubleInequalityReasoner</tt>.
+
** Improve pattern matching for associative operators.
 +
* Theory plug-in Branding (0.0.1) Initial version
 +
* Theory Core (4.0.0) Internal implementation changes.
 +
** Compatibility upgrade to Rodin 3.2
 +
** Support for INFIX extended predicate operators.
 +
** Various bugs fixed.
 +
* Theory help (2.0.0) User documentations.
 +
* Theory Keyboard (0.0.1) Initial version (A special plug-in for typesetting Theory).
 +
** Support for typesetting Real arithmetics (plus, unary minus, multiply, divide, less than, less than or equal, greater than, greater than or equal).
 +
* Theory Rule-based Prover (4.0.0)
 +
** Reasoners' input does not contain the proof-obligation context.
 +
** Use the current sequent's origin to get the proof-obligation context.
 +
** Bug fixed: translate formula to ensure they have the same formula factory.
 +
** Added version numbers for reasoners.
 +
** Automatic rewrite and inference tactics are re-implemented so that each rule application is visible in proof trees.
 +
* Theory UI (3.0.0)
  
−
=== Step2 ===
+
===== Version 3.0.0 =====
−
Implement the body of the reasoner :
+
''17th December 2014''
  
−
* the reasoner shall "<tt>implements IVersionedReasoner</tt>" thus <tt>getVersion()</tt> shall return a static integer giving the current version of our reasoner. 0 might not be a wrong choice for our first try. <tt>getReasonerID()</tt> shall return a unique ID. It MUST correspond to the id given in the reasoner extension we created, and is prefixed by the plugin id where it lays. Here, we didn't create any activator for our plugin, so no such constant prefix exists. So, let's create here something like :
+
Release target : Rodin 3.1
 +
* migration changes to Rodin 3.1
  
−
private static final String REASONER_ID = "org.eventb.doubleInequality.dblIneq";
+
===== Version 2.0.2 =====
 +
''10th July 2014''
  
−
You should now have something close to this :
+
Release target : Rodin 2.8
 +
* bug fixes.
  
−
public class DoubleInequalityReasoner implements IVersionedReasoner {
+
===== Version 2.0.1 =====
−
+
''24th June 2014''
−
private static final int VERSION = 0;
 
−
private static final String REASONER_ID = "org.eventb.doubleInequality.dblIneq";
 
−
 
−
@Override
 
−
public String getReasonerID() {
 
−
return REASONER_ID;
 
−
}
 
−
 
−
@Override
 
−
public int getVersion() {
 
−
return VERSION;
 
−
}
 
−
 
−
@Override
 
−
public IReasonerOutput apply(IProverSequent seq, IReasonerInput input,
 
−
IProofMonitor pm) {
 
−
 
−
        }
 
  
−
=== Step3 / Exercise ===
+
Release target : Rodin 2.8
 +
* bug fixes.
  
−
Implement the method public <tt>IReasonerOutput '''apply'''(IProverSequent seq, IReasonerInput input, IProofMonitor pm)</tt>. This method is the place where one shall create the proof rule to be applied from the input sequent <tt>seq</tt> and with the given input if needed.
+
===== Version 2.0.0 =====
−
Here is the list of tasks you have to perform in this <tt>apply()</tt> method :
+
''30th April 2014''
−
* get and check the input predicate a <= b,
 
−
* check the presence of the other hypothesis b <= a,
 
−
* make the new hypothesis a=b that will be in the antecedent produced by our rule,
 
−
* make the antecedent (see the picture above) where a <= b and b <= a are deselected(i.e. hidden) so that the tactic does not apply in unfinite loop,
 
−
* make the proof rule to return,
 
  
−
=== Step4 ===
+
Release target : Rodin 2.8
−
Here we see together the solution proposed for the implementation of the <tt>apply()</tt> method of our reasoner:
+
* Major changes in the usability.
 +
* Important bug fixes.
  
−
@Override
+
===== Version 1.3.2 =====
−
public IReasonerOutput apply(IProverSequent seq, IReasonerInput input, IProofMonitor pm) {
+
''20th April 2012''
  
−
* get and check the input predicate a <= b
+
Release target : Rodin 2.4
−
 
+
* Important bug fixes.  
−
NB : Here we suppose that the given input doesn't have any error. If it has, we shall return a <tt>reasonerFailure</tt>(See <tt>ProverFactory.reasonerFailure()</tt> method for more details).<br>
+
* Improvement of deployment and un-deployment wizards
−
We want our <tt>IReasonerInput</tt> to be a predicate input of the form "a <= b". Thus, there is an existing class to reuse : <tt>SinglePredInput</tt>.<br>
 
−
Please, have a look at <tt>IReasonerInput</tt> implementation hierarchy to see which kind of input classes exist and that you could reuse in your reasoners.<br>
 
−
[[Image:IReasonerInput.png|400px|center]]
 
  
−
Thus, here is what you should write :
+
===== Version 1.2 =====
 +
''15th August 2011''
  
−
  if (input.hasError()) {
+
Release target : Rodin 2.2.2
−
    return ProverFactory.reasonerFailure(this, input, input.getError());
+
* Bug fixes.  
−
  }
+
* Added capability to instantiate multiple theorems at once.
−
  final SinglePredInput predInput = (SinglePredInput) input;
+
* Added automatic tactic for expanding operator definitions RbPxd·
−
  final Predicate predicate = predInput.getPredicate();
 
−
  if (predicate.getTag() != Formula.LE) {
 
−
    return ProverFactory.reasonerFailure(this, input, "invalid input predicate");
 
−
  }
 
  
−
* check the presence of the other hypothesis b <= a
+
===== Version 1.1 =====
−
  // we are sure that the predicate is a relational predicate as we checked that getTag() == Formula.LE
+
''6th August 2011''
−
  final RelationalPredicate aLEb = (RelationalPredicate) predicate;
 
−
  final Expression a = aLEb.getLeft();
 
−
  final Expression b = aLEb.getRight();
 
−
  final FormulaFactory ff = seq.getFormulaFactory(); // we retrieve the formula factory
 
−
  final Predicate bLEa = ff.makeRelationalPredicate(Formula.LE, b, a, null); // we build b <= a
 
−
  if (!seq.containsHypotheses(Arrays.asList(aLEb, bLEa))) {
 
−
    return ProverFactory.reasonerFailure(this, input,"sequent does not contain required hypotheses");
 
−
  }
 
  
−
* make the new hypothesis a=b
+
Release target : Rodin 2.2.2
−
NB : we reuse the formula factory that we got from the sequent to create the new hypothesis <tt>a = b</tt> :
+
* Theory library first version.
−
  final Predicate aEqb = ff.makeRelationalPredicate(Formula.EQUAL, a, b, null);
+
* Bug fixes.
 +
* Improved UI.
  
−
* make the antecedent
+
===== Version 1.0 =====
−
  // we create the added hypothesis a = b
+
''8th July 2011''
−
  final Set<Predicate> addedHyps = Collections.singleton(aEqb);
 
−
  // we hide a <= b and b <= a
 
−
  final ISelectionHypAction hideIneqs = ProverFactory.makeHideHypAction(Arrays.asList(aLEb, bLEa));
 
−
  // we create our antecedent to be used in our proof rule
 
−
  final IAntecedent antecedent = ProverFactory.makeAntecedent(null, addedHyps, hideIneqs);
 
  
−
* make the proof rule to return
+
Release target : Rodin 2.2
−
 
 
−
  // We do not forget to say that a <= b (aLEb) and b <= a (bLEa) are needed for our rule to be applied
 
−
  final Set<Predicate> neededHyps = new HashSet<Predicate>();
 
−
  neededHyps.addAll(Arrays.asList(aLEb, bLEa));
 
−
 
−
  // We return the proof rule corresponding to DBL_INEQ
 
−
  return ProverFactory.makeProofRule(this, input, null, neededHyps, "Inequality Rewrites", antecedent);
 
−
 
−
  }
 
  
−
=== Step5 ===
+
* Bug fixes.
 +
* Added import relationships between theories.
 +
* Added experimental support for recursive definitions.
 +
* Improved project as well as workspace scope for mathematical and prover extensions.
 +
* Added tactic (xd) to expand all definitions.
 +
* Fixed support for polymorphic theorems.
  
−
As our input is actually a SinglePredInput, which as its name describes, holds a predicate, our reasoner is actually a specialisation of the abstract class SinglePredInputReasoner.
+
===== Version 0.8 =====
−
Please check the other proposed (e.g. published) types of reasoners corresponding to existing inputs among :
+
''22nd May 2011''
−
* SingleExprInputReasoner,
 
−
* SinglePredInputReasoner,
 
−
* SingleStringInputReasoner,
 
−
* EmptyInputReasoner,
 
−
* ForwardInfReasoner,
 
−
* HypothesisReasoner,
 
−
* XProverInputReasoner.
 
  
−
In our case, simply add the <tt>extends SinglePredInputReasoner</tt> to the declaration of the reasoner class.
+
Release target : Rodin 2.1.1
−
And this is all for our reasoner! Now let's add a tactic corresponding to it.
 
  
−
=== Step6 ===
+
* Bug fixes.
 +
* Added import relationships between theories.
 +
* Added experimental support for recursive definitions.
 +
* Added project as well as workspace scope for mathematical and prover extensions.
  
−
Now that we have the reasoner DoubleInequalityReasoner, we need to create a tactic to call this reasoner when possible.
+
===== Version 0.7 =====
−
We want this reasoner, for more convenience, to be applied automatically. Thus we define an auto-tactic that will call our reasoner.
+
''11th April 2011''
  
−
* Add the extension point <tt>org.eventb.core.seqprover.autoTactics</tt> to our plugin,
+
Bug fixes. Fixed for Rodin 2.1.1.
−
* create an extension ''autoTactic'' for a new tactic we will create here with :
 
−
:- ''id : dblIneqTac'',<br>
 
−
:- ''name : Double Inequality Tactic'',<br>
 
−
:- ''description : Applies Double Inequality Rule'',<br>
 
−
:- ''auto : place the boolean to <tt>true</tt> to let the tactic be automatic'',<br>
 
−
:- ''post : place the boolean to <tt>true</tt> so the tactic will no execute as a post tactic'',<br>
 
−
:- And now it remains the tactic ''class'' to create. So, create the tactic class <tt>DoubleInequalityTactic</tt> which <tt>implements ITactic</tt>.<br>
 
  
−
In this tactic, what we have to do is to calculate if the current proof tree node contains an application of the reasoner, and if it is the case, call the reasoner.
+
===== Version 0.6 =====
−
You can see that the only method to implement is : <tt>apply(IProofTreeNode ptNode, IProofMonitor pm)</tt>
+
''6th January 2011''
−
We will detail here, what one should do in this method:
 
  
−
@Override
+
Minor bug fixes and improvements to theories pretty printer.
−
public Object apply(IProofTreeNode ptNode, IProofMonitor pm) {
 
  
−
* First, we search for double inequalities ''a <= b'' and ''b <= a'' in the selected hypotheses. To search it, we traverse all the selected hypotheses via <tt>sequent.selectedHypIterable()</tt>.
+
===== Version 0.5 =====
 +
''28th October 2010''
  
−
final IProverSequent sequent = ptNode.getSequent();
+
This is the first release of the Theory plug-in with support for mathematical as well as prover extensions.
−
final FormulaFactory ff = sequent.getFormulaFactory();
 
−
  for (Predicate hyp : sequent.selectedHypIterable()) {
 
  
−
* Then, when we encounter one hypothesis of the form E <= F (e.g. hypothesis.getTag() == Formula.LE), then we build the hypothesis F <= E :
+
===Features Requests and Bugs===
−
if (hyp.getTag() == Formula.LE) {
+
Please do not hesitate to raise any issues with regards to usability as well as efficiency. Finally, please remember to report any bugs through the SourceForge portal.
−
final RelationalPredicate aLEb = (RelationalPredicate) hyp;
 
−
final Expression a = aLEb.getLeft();
 
−
final Expression b = aLEb.getRight();
 
−
final RelationalPredicate bLEa = ff.makeRelationalPredicate(Formula.LE, b, a, null);
 
  
−
* if the sequent contains this latter hypothesis, we call the reasoner DoubleInequalityReasoner (encapsulated in a tactic)
+
[[Category:Theory Plug-in]]
−
if(sequent.containsHypothesis(bLEa)) {
 
−
                return callDblIneqReasoner(ptNode, aLEb, pm);
 
−
  }
 
−
}
 
−
  }
 
−
  return "no double inequality hypotheses found";
 
−
}
 
−
 
−
As we need to construct the SinglePredInput with the hypothesis a <= b, and then apply our reasoner, the usual way to do this, is to encapsulate this reasoner call into a tactic. There is a facility to do that offered by <tt>BasicTactics.reasonerTac</tt>. Thus we write the following :
 
−
 
 
−
1  private Object callDblIneqReasoner(IProofTreeNode ptNode, final RelationalPredicate inputPred, IProofMonitor pm) {
 
−
2  final ITactic dblIneqTac = BasicTactics.reasonerTac(new DoubleInequalityReasoner(), new SinglePredInput(inputPred));
 
−
3  return dblIneqTac.apply(ptNode, pm);
 
−
4  }
 
−
where at line 2 we encapsulate the reasoner call, and at line 3, we apply the reasoner.
 
−
 
 
−
=== Conclusion ===
 
−
That's it for the addition of reasoners in the seqprover.
 
−
Now you can try it by creating a simple context for example, with the two hypotheses as axioms and another theorem such as a = 2.<br>
 
−
By running the auto-provers, you should see that the Inequality Rewrites is applied.
 
−
 
 
−
N.B: if you don't see any application of our reasoner, you might have forgotten to select the corresponding tactic to the auto tactic profile which is applied.
 
−
Go to ''Window > Prefences'', and then in ''Event-B category > Sequent Prover'', select the "Auto/Post Tactic" preferences and create a new profile and add the ''Double Inequality Tactic'' to it.<br />
 
−
You can select it from the list on the left within the profile editor (see the picture below):
 
−
 
 
−
[[Image:DBL_INEQ_Preferences.png|650px]]
 
−
 
 
−
{{Navigation|Previous= [[Extending_the_Proof_Obligation_Generator(How_to_extend_Rodin_Tutorial) | Generating the proof obligations]] | Up= [[Plug-in_Tutorial|How to extend Rodin Tutorial (Index)]]}}
 
−
 
 
−
[[Category:Developer documentation|*Index]]
 
−
[[Category:Rodin Platform|*Index]]
 
−
[[Category:Tutorial|*Index]]
 

Revision as of 13:11, 29 September 2021

Back to Theory Plug-in.

Follow this page for the latest on the Theory plug-in. The user manual is also provided together with the installation details.

News

  • 29th September 2021: Version 4.0.3 is released. It requires Rodin 3.5.
  • 4th June 2021: Version 4.0.2 is released. It requires Rodin 3.5.
  • 22th December 2020: Version 4.0.1 is released. It requires Rodin 3.5.
  • 19th December 2014: Version 3.0.o is released. It requires Rodin 3.1.
  • 10th July 2014: Version 2.0.2 is released. It requires Rodin 2.8.
  • 24th June 2014: Version 2.0.1 is released. It requires Rodin 2.8.
  • 30th April 2014: Version 2.0.0 is released. It requires Rodin 2.8. This release contains major changes in the features and accessibilities.
  • 20th April 2012: Version 1.3.2 is released. It requires Rodin 2.4.
  • 15th August 2011: Version 1.2 is released. It requires Rodin 2.2.2.
  • 6th August 2011: Version 1.1 is released. It requires Rodin 2.2.2.
  • 8th July 2011: Version 1.0 is released. It requires Rodin 2.2.
  • 22nd May 2011: Version 0.8 released. It is based on Rodin 2.1.1.
  • 11th April 2011: Version 0.7 released. It is based on Rodin 2.1.1.
  • 6th January 2011: Version 0.6 released. It is based on Rodin 2.0.1.
  • 28th October 2010: Version 0.5 released. It is based on Rodin 2.0.

Releases

Version 4.0.3

29th September 2021

Release target: Rodin 3.5

  • Bug fixes:
    • Operators that have parameters with the same name but different types are now handled correctly in both the editor and the prover (for rewriting the definition)
    • Theorems instantiated during proof are now correctly typed (in some cases, some type information was missing)
Version 4.0.2

4th June 2021

Release target: Rodin 3.5

  • Bug fixes:
    • Datatypes that have several type parameters are now serialized in the right order; it fixes some issues with proofs and proof replay.
    • Manually applied inference and rewrite rules are now replayed correctly (in some cases, their replay was displayed as uncertain).
Version 4.0.1

22th December 2020

Release target: Rodin 3.5

  • Bug fixes:
    • The theory plugin now takes into account updates in theories, as well as creating a theory after using it (there was a cache issue).
    • The error messages at launch about rule-based provers failing to find the context of the proof have been removed.
    • The dropdown list in theory imports is now usable (there was an off-by-one issue when selecting an element in the list).
    • Manually applying an inference rule no longer throws a NullPointerException.
    • It is now possible to rename theories.
    • The TheoryPath creation dialog box has been simplified.
  • Optimizations:
    • The proving interface is now much more responsive, even when a theory contains a lot of rewrite rules (we have implemented a cache of the places where a rewrite rule can apply).
    • The theory plugin now generates much simpler WD conditions, especially for the pred, succ, prj1, prj2, and id operators.
Version 4.0.0-RC1

10th April 2017

Release target: Rodin 3.2

  • AST Extensions (4.0.0) Major API change.
    • Compatibility upgrade to Rodin 3.2
    • Support for get operator position for INFIX extended predicate operators.
    • Improve pattern matching for associative operators.
  • Theory plug-in Branding (0.0.1) Initial version
  • Theory Core (4.0.0) Internal implementation changes.
    • Compatibility upgrade to Rodin 3.2
    • Support for INFIX extended predicate operators.
    • Various bugs fixed.
  • Theory help (2.0.0) User documentations.
  • Theory Keyboard (0.0.1) Initial version (A special plug-in for typesetting Theory).
    • Support for typesetting Real arithmetics (plus, unary minus, multiply, divide, less than, less than or equal, greater than, greater than or equal).
  • Theory Rule-based Prover (4.0.0)
    • Reasoners' input does not contain the proof-obligation context.
    • Use the current sequent's origin to get the proof-obligation context.
    • Bug fixed: translate formula to ensure they have the same formula factory.
    • Added version numbers for reasoners.
    • Automatic rewrite and inference tactics are re-implemented so that each rule application is visible in proof trees.
  • Theory UI (3.0.0)
Version 3.0.0

17th December 2014

Release target : Rodin 3.1

  • migration changes to Rodin 3.1
Version 2.0.2

10th July 2014

Release target : Rodin 2.8

  • bug fixes.
Version 2.0.1

24th June 2014

Release target : Rodin 2.8

  • bug fixes.
Version 2.0.0

30th April 2014

Release target : Rodin 2.8

  • Major changes in the usability.
  • Important bug fixes.
Version 1.3.2

20th April 2012

Release target : Rodin 2.4

  • Important bug fixes.
  • Improvement of deployment and un-deployment wizards
Version 1.2

15th August 2011

Release target : Rodin 2.2.2

  • Bug fixes.
  • Added capability to instantiate multiple theorems at once.
  • Added automatic tactic for expanding operator definitions RbPxd·
Version 1.1

6th August 2011

Release target : Rodin 2.2.2

  • Theory library first version.
  • Bug fixes.
  • Improved UI.
Version 1.0

8th July 2011

Release target : Rodin 2.2

  • Bug fixes.
  • Added import relationships between theories.
  • Added experimental support for recursive definitions.
  • Improved project as well as workspace scope for mathematical and prover extensions.
  • Added tactic (xd) to expand all definitions.
  • Fixed support for polymorphic theorems.
Version 0.8

22nd May 2011

Release target : Rodin 2.1.1

  • Bug fixes.
  • Added import relationships between theories.
  • Added experimental support for recursive definitions.
  • Added project as well as workspace scope for mathematical and prover extensions.
Version 0.7

11th April 2011

Bug fixes. Fixed for Rodin 2.1.1.

Version 0.6

6th January 2011

Minor bug fixes and improvements to theories pretty printer.

Version 0.5

28th October 2010

This is the first release of the Theory plug-in with support for mathematical as well as prover extensions.

Features Requests and Bugs

Please do not hesitate to raise any issues with regards to usability as well as efficiency. Finally, please remember to report any bugs through the SourceForge portal.

Retrieved from ‘https://wiki.event-b.org/index.php?title=Adding_Reasoners(How_to_extend_Rodin_Tutorial)&oldid=14479’