New Proof Rules: Difference between revisions

From Event-B
Jump to navigationJump to search
← Older edit
imported>Nicolas
mNo edit summary
imported>Mathieu
 
(5 intermediate revisions by 3 users not shown)
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.
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.




==Remove Membership for Range==
==Remove Membership for Range==


This is submitted as feature request 1942487 at sourceforge.
The work is related to the following rewriting rule:


[https://sourceforge.net/tracker2/?func=detail&aid=1942487&group_id=108850&atid=651672 1942487]
<math>  E \in a \upto b  ~~~\mathrel{\widehat{=}}~~~ a \leq E ~\land~ E \leq b  </math>
The request is about the following rewriting rule:
 
<math>  E \in a \upto b  ~~~\mathrel{\widehat{=}}~~~ a \leq E ~\land~ E \leq b  </math>


The rule has been implemented so that it can be applied both automatically and interactively.
The rule has been implemented so that it can be applied both automatically and interactively.
Line 21: Line 17:
==Automatic Rule for Overriding==
==Automatic Rule for Overriding==


This is submitted as feature request 1936295 at sourceforge.
The work is related to the following rewriting rule:


[http://sourceforge.net/tracker/index.php?func=detail&aid=1936295&group_id=108850&atid=651672 1936295]
<math>  p \ovl \ldots \ovl \emptyset \ovl \ldots q  ~~~\mathrel{\widehat{=}}~~~ p \ovl \ldots \ovl q  </math>
 
The request is about 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)
(i.e. removing <math>\emptyset</math> for overriding <math>\ovl</math> operator)
Line 36: Line 28:
==Automatically Apply De Morgan's Laws==
==Automatically Apply De Morgan's Laws==


This is submitted as feature request 1935674 at sourceforge.
The work is related to the following rewriting rules (De Morgan's Laws):


[http://sourceforge.net/tracker/index.php?func=detail&aid=1935674&group_id=108850&atid=651672 1935674]
<math>
 
The request is about the following rewriting rules (De Morgan's Laws):
 
<math>
\begin{array}{c}
\begin{array}{c}
\neg ( P \land \ldots \land Q )  ~~~\mathrel{\widehat{=}}~~~  \neg P \lor \ldots \lor \neg Q \\
\neg ( P \land \ldots \land Q )  ~~~\mathrel{\widehat{=}}~~~  \neg P \lor \ldots \lor \neg Q \\
Line 49: Line 37:
\neg (\exists x \qdot P)  ~~~\mathrel{\widehat{=}}~~~  \forall x \qdot \neg P
\neg (\exists x \qdot P)  ~~~\mathrel{\widehat{=}}~~~  \forall x \qdot \neg P
\end{array}
\end{array}
</math>  
</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.
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.
Line 55: Line 43:
==Automatically Rewrite <math>\dom(f) = S</math>==
==Automatically Rewrite <math>\dom(f) = S</math>==


This is submitted as feature request 1866809 at sourceforge.
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.


[http://sourceforge.net/tracker/index.php?func=detail&aid=1866809&group_id=108850&atid=651672 1866809]
<math>
 
The request 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}
\begin{array}{l}
f \in S \trel T \\
f \in S \trel T \\
Line 68: Line 52:
f \in S \tbij T
f \in S \tbij T
\end{array}
\end{array}
</math>
</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.
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.
Line 74: Line 58:
==Interactively Rewrite <math>B \subset A</math>==
==Interactively Rewrite <math>B \subset A</math>==


This is submitted as feature request 1834715 at sourceforge.
The work is about providing support for interactively proving <math>B \subset A</math> according to the following rewriting rules.
 
[http://sourceforge.net/tracker/index.php?func=detail&aid=1834715&group_id=108850&atid=651672 1834715]
 
The request 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>
<math> B \subset A  ~~~\mathrel{\widehat{=}}~~~ B \subseteq A ~\land~ \lnot B = A </math>


The rule has been implemented so that it can be applied both automatically and interactively.
The rule has been implemented so that it can be applied both automatically and interactively.
Line 86: Line 66:
* 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>.
* 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>.


* 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.
* Interactively: The <math>\subset</math> symbol is redden in the formula (either goal or hypotheses) and is applied only to the sub-formula as indicated by the user.




[[Category:Event-B]]
[[Category:Event-B]]
[[Category:Proof]]

Latest revision as of 12:53, 12 August 2009

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.


Remove Membership for Range

The work is related to the following rewriting rule:

E \in a \upto b ~~~\mathrel{\widehat{=}}~~~ a \leq E ~\land~ E \leq b

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 E \in a \upto b.
  • Interactively: The \in symbol is redden in the formular (either goal or hypotheses) and is applied only to the sub-formula as indicated by the user.


Automatic Rule for Overriding

The work is related to the following rewriting rule:

p \ovl \ldots \ovl \emptyset \ovl \ldots q ~~~\mathrel{\widehat{=}}~~~ p \ovl \ldots \ovl q

(i.e. removing \emptyset for overriding \ovl 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):

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

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 \dom(f) = S

The work is about rewriting automatically \dom(f) \mathrel{\widehat{=}} S for selected hypotheses and goal if there is a hypothesis that f is a total function from S, e.g.

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

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 B \subset A

The work is about providing support for interactively proving B \subset A according to the following rewriting rules.

B \subset A ~~~\mathrel{\widehat{=}}~~~ B \subseteq A ~\land~ \lnot B = A

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 B \subset A.
  • Interactively: The \subset symbol is redden in the formula (either goal or hypotheses) and is applied only to the sub-formula as indicated by the user.
Retrieved from ‘https://wiki.event-b.org/index.php?title=New_Proof_Rules&oldid=6258’