Difference between revisions of "Negation Normal Form"

From Event-B
Jump to navigationJump to search
imported>Billaude
(Description and implementation of the Negation Normal Form)
 
imported>Laurent
Line 19: Line 19:
  
  
There is no rule implemented for that type of expression : <math> \lnot (P \leqv Q) </math> (which is equivalent to <math> (\lnot  P \leqv Q))</math> The way the reasoner 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 is ambiguous. Here is an example showing that difficulty :  
+
There is no rule implemented for that type of expression : <math> \lnot (P \leqv Q) </math> (which is equivalent to <math> (\lnot  P \leqv Q))</math> The way the reasoner 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 :  
  
  
Line 28: Line 28:
  
 
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)
 
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 =
 
= Implementation =

Revision as of 15:43, 13 April 2011

This page describe the Negation Normal Form used in Rodin and show how it has been implemented.

Definition

A logical formula is in its Negation Normal Form if negation occurs only on atomic expression. To achieve this, rules already defined are reused :

SIMP_NOT_NOT : 	\lnot\, \lnot\, P \;\;\defi\;\; P

DISTRI_NOT_AND :   \lnot\,(P \land  Q) \;\;\defi\;\;  \lnot\, P \lor  \lnot\, Q

DISTRI_NOT_OR :   \lnot\,(P \lor  Q) \;\;\defi\;\;  \lnot\, P \land  \lnot\, Q

DERIV_NOT_IMP :   \lnot\,(P \limp  Q) \;\;\defi\;\;  P \land  \lnot\, Q

DERIV_NOT_FORALL :   \lnot\, \forall x \qdot  P \;\;\defi\;\;  \exists x \qdot  \lnot\, P

DERIV_NOT_EXISTS :   \lnot\, \exists x \qdot  P \;\;\defi\;\;  \forall x \qdot  \lnot\, P


There is no rule implemented for that type of expression :  \lnot (P \leqv Q) (which is equivalent to  (\lnot  P \leqv Q)) The way the reasoner will work is yet to be defined. Since the "\leqv" is to be kept, the choice on which predicate the not will be applied to is ambiguous. Here is an example showing that difficulty :


\lnot(A \leqv \lnot (B \lor C)) (1) which is equivalent to \lnot(A \leqv (\lnot B \land \lnot C)) (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 \lnot on a member containing already a \lnot. But it can be hard to find an expression with a \lnot which has already been put in its Negation Normal Form as for the right member in (2)

Implementation

Tactics

When an expression with a negation is matched, rules are applied following a prefix reading of that expression.

\lnot(A \land \lnot (B \lor C))

\lnot A \lor \lnot\lnot (B \lor C)

\lnot A \lor (B \lor C)

INSTEAD OF

\lnot(A \land \lnot (B \lor C))

\lnot(A \land (\lnot B \land \lnot C))

\lnot A \lor \lnot(\lnot B \land \lnot C)

\lnot A \lor (\lnot\lnot B \lor \lnot\lnot C)

\lnot A \lor (B \lor \lnot\lnot C)

\lnot A \lor (B \lor C)

In that way, tree proof is not unnecessarily complicated, and so more legible. The space used on disk is also smaller.