imported>Mathieu |
imported>Nicolas |
| Line 1: |
Line 1: |
| − | This document describes the set of newly added reasoners for improving the usability of the prover within Rodin Platform. The work has been done originally by Stephan Merkli, Michael Schaufelberger and David Simmen as their project for an object oriented programming course at ETH Zürich. The aim of the work is to try out the extensibility feature of the RODIN platform related to the prover. The rules are added using as various plug-ins with most of the work done in a declarative fashion. Moreover the new features are also tested using the pre-defined framework which has been set-up during the development of the RODIN platform. The rules are of different types: automatic/interactive rewriting or more general inference rules.
| + | In this page are presented various proof obligations commands that can be run from the Event-B Explorer as follows: |
| | | | |
| | + | [[Image:PO_Commands.png]] |
| | | | |
| − | ==Remove Membership for Range==
| + | These commands are run on all POs located under the node(s) selected in the explorer. The selection can be a whole project, a model (context/machine), the 'Proof Obligations' node (equivalent to selecting the corresponding model), an element type (Axioms/Invariants/Events), a particular element (axm12, inv314, …), a particular PO (INITIALISATION/inv2/INV, …), or any combination of selectable nodes (multiselection using the CTRL key). |
| | | | |
| − | The work is related to the following rewriting rule:
| + | == Retry Auto Provers == |
| | | | |
| − | <math> E \in a \upto b ~~~\mathrel{\widehat{=}}~~~ a \leq E ~\land~ E \leq b </math>
| + | As the name suggests, this command runs the Auto Provers on selected POs. When the 'Prove Automatically' option is turned off, it's a convenient way to manually trigger auto proving on the desired (set of) PO(s). |
| | | | |
| − | The rule has been implemented so that it can be applied both automatically and interactively.
| + | It may also be used after changing the Auto Prover preferences, in order to check whether the new prover configuration allows to discharge a given (set of) PO(s). |
| | | | |
| − | * Automatically: The rule can be chosen from the Preferences of the Sequent Prover to be run as a part of the Automatic Prover or as a part of the Post-Tactic. The rewriting is carried out to all sub-formulas of the form <math>E \in a \upto b</math>.
| + | == Recalculate Auto Status == |
| | | | |
| − | * Interactively: The <math>\in</math> symbol is redden in the formular (either goal or hypotheses) and is applied only to the sub-formula as indicated by the user.
| + | {{TODO}} |
| | | | |
| | + | == Proof Replay on Undischarged POs == |
| | | | |
| − | ==Automatic Rule for Overriding==
| + | {{TODO}} |
| | | | |
| − | The work is related to the following rewriting rule:
| |
| | | | |
| − | <math> p \ovl \ldots \ovl \emptyset \ovl \ldots q ~~~\mathrel{\widehat{=}}~~~ p \ovl \ldots \ovl q </math>
| |
| | | | |
| − | (i.e. removing <math>\emptyset</math> for overriding <math>\ovl</math> operator)
| |
| | | | |
| − | The rule is added so that it can be applied automatically. User can choose the rule from the Preferences of the Sequent Prover, so that it can be run as a part of the Automatic Prover or as a part of the Post-Tactic. The rewriting is carried out to all sub-formulas of the form that match the left-hand side of the rule.
| |
| | | | |
| | | | |
| − | ==Automatically Apply De Morgan's Laws==
| |
| | | | |
| − | The work is related to the following rewriting rules (De Morgan's Laws):
| |
| | | | |
| − | <math>
| |
| − | \begin{array}{c}
| |
| − | \neg ( P \land \ldots \land Q ) ~~~\mathrel{\widehat{=}}~~~ \neg P \lor \ldots \lor \neg Q \\
| |
| − | \neg (P \lor \ldots \lor Q) ~~~\mathrel{\widehat{=}}~~~ \neg P \land \ldots \land \neg Q \\
| |
| − | \neg (\forall x \qdot P) ~~~\mathrel{\widehat{=}}~~~ \exists x \qdot \neg P \\
| |
| − | \neg (\exists x \qdot P) ~~~\mathrel{\widehat{=}}~~~ \forall x \qdot \neg P
| |
| − | \end{array}
| |
| − | </math>
| |
| | | | |
| − | Currently, these rewriting rules can be invoked manualy during interactive proofs. The rules is added so that user can choose from the Preferences of the Sequent Prover, so that they can be run as a part of the Automatic Prover or as a part of the Post-Tactic. The rewriting is recursively carried out to all sub-formulas of the form that match the left-hand side of the one of the rule.
| |
| | | | |
| − | ==Automatically Rewrite <math>\dom(f) = S</math>==
| |
| | | | |
| − | The work is about rewriting automatically <math>\dom(f) \mathrel{\widehat{=}} S</math> for selected hypotheses and goal if there is a hypothesis that <math>f</math> is a total function from <math>S</math>, e.g.
| |
| | | | |
| − | <math>
| |
| − | \begin{array}{l}
| |
| − | f \in S \trel T \\
| |
| − | f \in S \tfun T \\
| |
| − | f \in S \tinj T \\
| |
| − | f \in S \tbij T
| |
| − | \end{array}
| |
| − | </math>
| |
| | | | |
| − | The rule is added so that it can be applied automatically. User can choose the rule from the Preferences of the Sequent Prover, so that it can be run as a part of the Automatic Prover or as a part of the Post-Tactic.
| |
| | | | |
| − | ==Interactively Rewrite <math>B \subset A</math>==
| |
| | | | |
| − | The work is about providing support for interactively proving <math>B \subset A</math> according to the following rewriting rules.
| |
| | | | |
| − | <math> B \subset A ~~~\mathrel{\widehat{=}}~~~ B \subseteq A ~\land~ B \neq A </math>
| |
| | | | |
| − | The rule has been implemented so that it can be applied both automatically and interactively.
| |
| | | | |
| − | * Automatically: The rule can be chosen from the Preferences of the Sequent Prover to be run as a part of the Automatic Prover or as a part of the Post-Tactic. The rewriting is carried out to all sub-formulas of the form <math>B \subset A</math>.
| + | {{TODO|Category}} |
| − | | |
| − | * Interactively: The <math>\subset</math> symbol is redden in the formular (either goal or hypotheses) and is applied only to the sub-formula as indicated by the user.
| |
| − | | |
| − | | |
| − | [[Category:Event-B]]
| |
In this page are presented various proof obligations commands that can be run from the Event-B Explorer as follows:
These commands are run on all POs located under the node(s) selected in the explorer. The selection can be a whole project, a model (context/machine), the 'Proof Obligations' node (equivalent to selecting the corresponding model), an element type (Axioms/Invariants/Events), a particular element (axm12, inv314, …), a particular PO (INITIALISATION/inv2/INV, …), or any combination of selectable nodes (multiselection using the CTRL key).
Retry Auto Provers
As the name suggests, this command runs the Auto Provers on selected POs. When the 'Prove Automatically' option is turned off, it's a convenient way to manually trigger auto proving on the desired (set of) PO(s).
It may also be used after changing the Auto Prover preferences, in order to check whether the new prover configuration allows to discharge a given (set of) PO(s).
Recalculate Auto Status
TODO
Proof Replay on Undischarged POs
TODO
TODO: Category
