Difference between pages "Negation Normal Form" and "New Proof Rules"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Laurent
(Fully edited explanations and examples)
 
imported>Son
 
Line 1: Line 1:
−
This page describes the design of a tactic for putting a sequent in Negation Normal Form, as requested by
+
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 add using as various plug-ins with most the work are done in a declarative fashion. Moreover the new feature also be 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.
−
[https://sourceforge.net/tracker/index.php?func=detail&aid=3137893&group_id=108850&atid=651672 Feature Request #3137893].
 
  
−
= Objective =
 
  
−
A predicate is in Negation Normal Form when negation occurs only on atomic expression. To compute such a normal form, the following rewrite rules (which are already implemented in Rodin) are used:
+
==Remove Membership for Range==
−
:SIMP_NOT_NOT: <math> \lnot\, \lnot\, P \;\;\defi\;\; P </math>
 
−
:DISTRI_NOT_AND: <math>  \lnot\,(P \land  Q) \;\;\defi\;\;  \lnot\, P \lor  \lnot\, Q </math>
 
−
:DISTRI_NOT_OR: <math>  \lnot\,(P \lor  Q) \;\;\defi\;\;  \lnot\, P \land  \lnot\, Q </math>
 
−
:DERIV_NOT_IMP: <math>  \lnot\,(P \limp  Q) \;\;\defi\;\;  P \land  \lnot\, Q </math>
 
−
:DERIV_NOT_FORALL: <math>  \lnot\, \forall x \qdot  P \;\;\defi\;\;  \exists x \qdot  \lnot\, P </math>
 
−
:DERIV_NOT_EXISTS: <math>  \lnot\, \exists x \qdot  P \;\;\defi\;\;  \forall x \qdot  \lnot\, P </math>
 
  
−
However, no rule has been defined for the case where the inner predicate is an equivalence, such as <math> \lnot (P \leqv Q) </math>, which is equivalent to both <math> \lnot  P \leqv Q</math> and <math>P \leqv\lnot Q</math>. Currently, the tactic will not do anything for such predicates.
+
The work is related to the following rewriting rule:
  
−
= Analysis =
+
<math>  E \in a \upto b  ~~~\mathrel{\widehat{=}}~~~ a \leq E ~\land~ E \leq b  </math>
  
−
For equivalence predicate, as the tactic is to be designed for interactive use, we prefer to keep the equivalence predicate (rather than translate it to e.g.,  double implication). However, it is not clear how to decide which sub-predicate should get the negation.  Some cases seem obvious.  For instance, if one of the child is itself a negation, it seems a good idea to push the negation to this child (where both negations will cancel each other). Similarly, if one child is atomic, pushing the negation to this child seems also a good candidate.
+
The rule has been implemented so that it can be applied both automatically and interactively.
  
−
However, in the general case, it is not easy to decide to which child the negation shall be pushed downto. For instance, consider predicate
+
* 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>.
−
:<math>\lnot(A \leqv (\lnot B \land\lnot C))</math>
 
−
If we push negation to the left-hand child, we obtain the equivalent predicate
 
−
:<math>\lnot A \leqv (\lnot B \land\lnot C)</math>
 
−
But, if we push it to the right-hand child, we get the normal form
 
−
:<math> A \leqv (B \or C)</math>
 
−
which is highly preferable, as it is simpler to read.
 
  
−
It is not yet clear whether there is a good criterion for deciding which child to go for.
+
* 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.
  
−
= Implementation =
 
  
−
The tactic shall apply to all visible hypotheses and the goal of a sequent. It should apply repeatedly the above rewrite rules until all these predicates are in Negation Normal Form.
+
==Automatic Rule for Overriding==
  
−
However, care should be taken when organising the applications of these rules.  They should be applied following a pre-order traversal of the predicate, to avoid undoing and redoing several times the same operations. This can be easily shown in the following example.
+
The work is related to the following rewriting rule:
  
−
When rewrite rules are applied in the right order, the following rewrites are performed
+
<math> p \ovl \ldots \ovl \emptyset \ovl \ldots q  ~~~\mathrel{\widehat{=}}~~~ p \ovl \ldots \ovl q  </math>
−
:<math>\lnot(A \land \lnot (B \lor C))</math>
 
−
:<math>\lnot A \lor \lnot\lnot (B \lor C)</math>
 
−
:<math>\lnot A \lor (B \lor C)</math>            
 
  
−
However, if another order is used, one could get a much longer rewriting chain, such as
+
(i.e. removing <math>\emptyset</math> for overriding <math>\ovl</math> operator)
−
:<math>\lnot(A \land \lnot (B \lor C))</math>
+
 
−
:<math>\lnot(A \land (\lnot B \land \lnot C))</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 rewriting is carried out to all sub-formulas of the form that match the left-hand side of the rule.
−
:<math>\lnot A \lor \lnot(\lnot B \land \lnot C)</math>
+
 
−
:<math>\lnot A \lor (\lnot\lnot B \lor \lnot\lnot C)</math>
+
 
−
:<math>\lnot A \lor (B \lor \lnot\lnot C)</math>
+
==Automatically Apply De Morgan's Laws==
−
:<math>\lnot A \lor (B \lor C)</math>
+
 
 +
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>.
 +
 
 +
* 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]]

Revision as of 14:05, 27 January 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 add using as various plug-ins with most the work are done in a declarative fashion. Moreover the new feature also be 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~ B \neq 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 formular (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=Negation_Normal_Form&oldid=6255’