Difference between revisions of "Adding Reasoners(How to extend Rodin Tutorial)"
imported>Tommy m (→Principles) |
imported>Tommy m (→In this part) |
||
Line 17: | Line 17: | ||
|} | |} | ||
− | 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. | + | 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". Moreover, <math>\textbf{H}</math> is the set of selected hypotheses from the input sequent, and <math> a \leq b,\;b \leq a\;\vdash \;\; \textbf{G}</math> is the antecedent of the rule (i.e. a child node to be proved). |
=== Step1 === | === Step1 === |
Revision as of 11:03, 11 October 2010
Contents
Principles
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.
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 rewriting rule list) or inference rules (see 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).
In this part
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. The rule, coded within the reasoner, that we want to apply is the following:
![]() |
DBL_INEQ |
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 , whatever the goal of this sequent. We will say that
are the "Needed Hypotheses". Moreover,
is the set of selected hypotheses from the input sequent, and
is the antecedent of the rule (i.e. a child node to be proved).