Negation Normal Form - Revision history

imported>Laurent: Fully edited explanations and examples

2011-04-13T16:48:01Z

Fully edited explanations and examples

@@ 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
-= Definition =
+= 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 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>
+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
-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.
 = 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.
-<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
-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

imported>Laurent: /* Definition */

2011-04-13T16:02:59Z

Definition

← Older revision		Revision as of 16:02, 13 April 2011
Line 3:		Line 3:
	= Definition =		= 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 :		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 :

	SIMP_NOT_NOT : <math> \lnot\, \lnot\, P \;\;\defi\;\; P </math>		SIMP_NOT_NOT : <math> \lnot\, \lnot\, P \;\;\defi\;\; P </math>
Line 17:		Line 17:
	DERIV_NOT_EXISTS : <math> \lnot\, \exists x \qdot P \;\;\defi\;\; \forall 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>. 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 :

	~~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 :

imported>Laurent: /* Tactics */

2011-04-13T15:45:28Z

Tactics

← Older revision		Revision as of 15:45, 13 April 2011
Line 33:		Line 33:
	== Tactics ==		== Tactics ==

	When ~~an expression~~ with a negation is matched, rules are applied following a ~~prefix reading~~ of that ~~expression~~.		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 \land \lnot (B \lor C))</math>
Line 55:		Line 55:
	<math>\lnot A \lor (B \lor C)</math>		<math>\lnot A \lor (B \lor C)</math>

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

imported>Laurent: /* Definition */

2011-04-13T15:43:50Z

Definition

← Older revision		Revision as of 15:43, 13 April 2011
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 =

imported>Billaude: Description and implementation of the Negation Normal Form

2011-04-13T10:29:22Z

Description and implementation of the Negation Normal Form

New page

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 : <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>

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 :

<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 an expression with a negation is matched, rules are applied following a prefix reading of that expression.

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

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