Difference between pages "Negation Normal Form" and "Proof Obligation Commands"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Laurent
 
imported>Nicolas
 
Line 1: Line 1:
−
This page describe the Negation Normal Form used in Rodin and show how it has been implemented.
+
In this page are presented various proof obligations commands that can be run from the Event-B Explorer as follows:
  
−
= Definition =
+
[[Image:PO_Commands.png]]
  
−
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 reused :
+
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).
  
−
SIMP_NOT_NOT : <math> \lnot\, \lnot\, P \;\;\defi\;\; P </math>
+
== Retry Auto Provers ==
  
−
DISTRI_NOT_AND : <math>  \lnot\,(P \land  Q) \;\;\defi\;\;  \lnot\, P \lor  \lnot\, Q </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).
  
−
DISTRI_NOT_OR : <math>  \lnot\,(P \lor  Q) \;\;\defi\;\;  \lnot\, P \land  \lnot\, Q </math>
+
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).
  
−
DERIV_NOT_IMP : <math>  \lnot\,(P \limp  Q) \;\;\defi\;\;  P \land  \lnot\, Q </math>
+
== Recalculate Auto Status ==
  
−
DERIV_NOT_FORALL : <math>  \lnot\, \forall x \qdot  P \;\;\defi\;\;  \exists x \qdot  \lnot\, P </math>
+
{{TODO}}
  
−
DERIV_NOT_EXISTS : <math>  \lnot\, \exists x \qdot  P \;\;\defi\;\;  \forall x \qdot  \lnot\, P </math>
+
== Proof Replay on Undischarged POs ==
  
−
However, no rule has been defined for the case where the inner predicate is an equivalence, such as <math> \lnot (P \leqv Q) </math>. The latter is equivalent to both <math> \lnot  P \leqv Q</math> and <math>P \leqv\lnot Q</math>. In this latter case, the way the tactic will work is yet to be defined. Since the "<math>\leqv</math>" is to be kept, the choice on which predicate the not will be applied to is ambiguous. Here is an example showing that difficulty :
+
{{TODO}}
  
  
−
<math>\lnot(A \leqv \lnot (B \lor C))</math> (1) which is equivalent to <math>\lnot(A \leqv (\lnot B \land \lnot C))</math> (2)
 
  
  
−
A solution would be to applied systematically on the left expression. In that case, simple simplification in the right member as in (1) would not be applied, thus complicating the left expression.
 
  
−
A better solution would to apply the <math>\lnot</math> on a member containing already a <math>\lnot</math>. But it can be hard to find an expression with a <math>\lnot</math> which has already been put in its Negation Normal Form as for the right member in (2)
 
  
−
= Implementation =
 
  
−
== Tactics ==
 
  
−
When a predicate with a negation is matched, rules are applied following a pre-order traversal of that predicate.
 
  
−
<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>             
 
  
−
INSTEAD OF                                 
 
  
−
<math>\lnot(A \land \lnot (B \lor C))</math>
 
  
−
<math>\lnot(A \land (\lnot B \land \lnot C))</math>
 
  
−
<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>
 
  
−
<math>\lnot A \lor (B \lor C)</math>
+
{{TODO|Category}}
−
 
 
−
This way, tree proof is not unnecessarily complicated, and so more legible. The space used on disk is also smaller.
 

Revision as of 16:56, 4 March 2010

In this page are presented various proof obligations commands that can be run from the Event-B Explorer as follows:

PO Commands.png

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

Retrieved from ‘https://wiki.event-b.org/index.php?title=Negation_Normal_Form&oldid=6559’