Talk:Clausal normal form
|WikiProject Mathematics||(Rated Stub-class, Low-priority)|
The first rule under "Skolemize" is not correct. The quantifer on the rewritten form should still be a universal quantifier. Otherwise the skolem function created by the second rule could always be a skolem constant by eliminating the universal quantifier with the first rule.
I went ahead and edited the page to correct the skolemization error mentioned above.
(I can't sign with my new account name, because Wikipedia somehow timed out my registration email.)
- I don't quite understand the first sentece -- it does suggest that Clausal normal form is also called Conjunctive Normal Form but later on in the procedure shows that they are indeed not equivalent. Moreover the page contains no actual defintion other than through normalisation algorithm, one which quickly decides whether a given formula is in normal form or not. Balrog-kun (talk) 00:54, 20 June 2008 (UTC)
- I find the definition unambiguous, if maybe improvable. However, an "algorithm" for checking if a formula is in normal form is not a normalization algorithm. A normalization algorithm is the one given below, which transforms a formula into Clausal normal form. Anyway, I agree that this should be merged within Conjunctive Normal Form and become a section there.--Blaisorblade (talk) 20:17, 29 January 2011 (UTC)