Talk:Negation normal form
|WikiProject Mathematics||(Rated Stub-class, Low-priority)|
Please explain what this means
- I believe that it means that what is on the left side of the implication ( ) can be rewritten as what is on the right side of the implication ( ). 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, for this. I suggest that we change the in the article
I think that using would be really bad, because then it would be virtually impossible to figure out where one formula stops and another starts since 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 () notation is used in the other articles as well.. -- Obradović Goran (talk 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 is used for implication and is used for rewrite. That said, I don't think this is a good choice, and here's why: the "heavier" 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, 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 188.8.131.52 (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.
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, and 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.184.108.40.206 (talk) 12:59, 10 September 2016 (UTC)