Negation Normal Form: Difference between revisions

From Event-B
Jump to navigationJump to search
imported>Laurent
imported>Laurent
Fully edited explanations and examples
 
(One intermediate revision by the same user not shown)
Line 1: Line 1:
This page describe the Negation Normal Form used in Rodin and show how it has been implemented.
This page describes the design of a tactic for putting a sequent in Negation Normal Form, as requested by
[https://sourceforge.net/tracker/index.php?func=detail&aid=3137893&group_id=108850&atid=651672 Feature Request #3137893].


= Definition =
= Objective =


A logical formula is in its Negation Normal Form if negation occurs only on atomic expression. To achieve this, rules already defined are reused :  
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:
: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>


SIMP_NOT_NOT : <math> \lnot\, \lnot\, P \;\;\defi\;\; 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.


DISTRI_NOT_AND : <math>  \lnot\,(P \land  Q) \;\;\defi\;\;  \lnot\, P \lor  \lnot\, Q </math>
= Analysis =


DISTRI_NOT_OR : <math>  \lnot\,(P \lor Q) \;\;\defi\;\; \lnot\, P \land  \lnot\, Q </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.


DERIV_NOT_IMP : <math> \lnot\,(P \limp  Q) \;\;\defi\;\;  P \land \lnot\, Q </math>
However, in the general case, it is not easy to decide to which child the negation shall be pushed downto. For instance, consider predicate
:<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.


DERIV_NOT_FORALL : <math>  \lnot\, \forall x \qdot  P \;\;\defi\;\;  \exists x \qdot  \lnot\, P </math>
It is not yet clear whether there is a good criterion for deciding which child to go for.
 
DERIV_NOT_EXISTS : <math>  \lnot\, \exists x \qdot  P \;\;\defi\;\;  \forall x \qdot  \lnot\, P </math>
 
 
 
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 :
 
 
<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 =
= Implementation =


== Tactics ==
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.
 
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>
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.


<math>\lnot A \lor (B \lor C)</math>
When rewrite rules are applied in the right order, the following rewrites are performed
:<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>            


This way, tree proof is not unnecessarily complicated, and so more legible. The space used on disk is also smaller.
However, if another order is used, one could get a much longer rewriting chain, such as
:<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>

Latest revision as of 16:48, 13 April 2011

This page describes the design of a tactic for putting a sequent in Negation Normal Form, as requested by 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:

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

However, no rule has been defined for the case where the inner predicate is an equivalence, such as  \lnot (P \leqv Q) , which is equivalent to both  \lnot  P \leqv Q and P \leqv\lnot Q. Currently, the tactic will not do anything for such predicates.

Analysis

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.

However, in the general case, it is not easy to decide to which child the negation shall be pushed downto. For instance, consider predicate

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

If we push negation to the left-hand child, we obtain the equivalent predicate

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

But, if we push it to the right-hand child, we get the normal form

 A \leqv (B \or C)

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.

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.

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.

When rewrite rules are applied in the right order, the following rewrites are performed

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

However, if another order is used, one could get a much longer rewriting chain, such as

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