Talk:Negation normal form

Syntax

Please explain what this means

$\lnot (\forall x.G)\to \exists x.\lnot G$

$\lnot (\exists x.G)\to \forall x.\lnot G$

Thank you, --Abdull (talk) 14:00, 19 June 2008 (UTC)

I believe that it means that what is on the left side of the implication ( $\lnot (\forall x.G)$ ) can be rewritten as what is on the right side of the implication ( $\exists x.\lnot G$ ). This is correct, but it took me a lot of time to understand that this is what it means, because I never saw that someone uses implication for that. Usually people use logical equivalence, $\equiv$ for this. I suggest that we change the in the article

$\lnot (\forall x.G)\to \exists x.\lnot G$

into

$\lnot (\forall x.G)\equiv \exists x.\lnot G$

-- Obradović Goran (ta^lk 15:42, 3 September 2008 (UTC)

I would propse $\Rightarrow$ or $\rightsquigarrow$ because we are describing a transformation of the formula, the equivalences you suggest is the reason that this transformation is safe. Taemyr (talk) 13:35, 9 September 2008 (UTC)

Actually, I note that $\to$ is used at term rewriting. It's perhaps best to leave it as is unless a standard is adopted that another symbol should be used. Taemyr (talk) 13:43, 9 September 2008 (UTC)

I think that using $\Rightarrow$ would be really bad, because then it would be virtually impossible to figure out where one formula stops and another starts since $\Rightarrow$ is FOL connective as well (at least, in numerous books that symbol is used for logical implication).

How about using this approach. Look at this Artificial intelligence book (it's in Serbian, but it will illustrate my point). On the page 55 is given the PRENEX algorithm (very similar to the NNF algorithm). Steps 1 and 2 are: As long as possible, apply the following logical equivalences. We could say the same in this article. Mathematician would understand what it means (current solution is confusing), and we could have additional explanation for the non-mathematician.

So, my suggestion is: As long as possible, apply the following logical equivalences (i.e. rewrite left side of the formula with the right side). But then again, if this ($\to$) notation is used in the other articles as well.. -- Obradović Goran (ta^lk 04:44, 15 September 2008 (UTC)

I believe that the easiest way to handle the issue of the two different right arrow symbols is simply to add a sentence to the discussion of the rewrite rules to clarify that $\Rightarrow$ is used for implication and $\rightarrow$ is used for rewrite. That said, I don't think this is a good choice, and here's why: the "heavier" $\Rightarrow$ is what jumps out at the reader, but that is the object-level notation. In this case the rewrite operator is at the meta level, and so is more important. It is the operator that should jump out at the reader. Unfortunately, that's exactly the reverse of what the existing symbology does. The logical equivalence symbol, $\equiv$ is a poor choice of substitute, because the equivalence relation is symmetric, whereas the rewrite relationship is directional. For now I will simply edit the page to explain the existing symbology. Rpgoldman (talk) 22:23, 5 June 2017 (UTC)

Undid last revision on NNF, the paragraph was simply wrong (checking a solution is still polynomial in NNF), and did not provide any value. — Preceding unsigned comment added by 132.231.65.155 (talk) 18:40, 10 December 2015 (UTC) $

Missing => Rule

Did a small edit and replaced the rewriting rules by exactly the rules from Handbook of Automated Reasoning 1, p. 204. These rules also consider the case of eliminating implication. Without this elimination we don't arrive at the negation normal form, which should only contain disjunction and conjunction.

Jan Burse (talk) 09:49, 21 March 2016 (UTC)

confused

In the present form the article is quite confused. What are "variables"? Perhaps they should be called atomic formulas, or proposition symbols in the case of propositional calculus. In fact, the article confuses propositional calculus and predicate calculus. The sentence "Negation normal form is not a canonical form: for example, $a\land (b\lor \lnot c)$ and $(a\land b)\lor (a\land \lnot c)$ are equivalent, and are both in negation normal form." is misleading, since the above formulas are in fact in "canonical" disjunctive, resp., conjunctive normal form. I guess that if the reader does not already know what nnf is, (s)he can hardly understand what nnf is, reading the article.78.15.176.53 (talk) 12:59, 10 September 2016 (UTC)

"and the number of occurrences of ¬ may double"

I wonder what the source and the reasoning for this statement is? I think the statement is not correct either, for example, ¬(A∧B∧C) is ¬A∨¬B∨¬C in NNF (more than double). --88.130.53.85 (talk) 21:32, 15 October 2019 (UTC)

You are correct that the claim is wrong, and your counter-example is a good one. A correct way to support "can increase the size of a formula only linearly" would be to observe that the final formula has at most as many negations as the original formula had variables. 108.180.81.240 (talk) 22:28, 8 September 2022 (UTC)