Talk:Clausal normal form

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.

68.41.169.151 (talk) 14:22, 1 June 2008 (UTC)[reply]

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

68.41.169.151 (talk) 14:43, 1 June 2008 (UTC)[reply]

Shouldn't this page be merged with Conjunctive Normal Form? 169.232.78.24 (talk)

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)[reply]

Clause Normal Form and Conjunctive Normal Form are not strictly identical, but they are isomorphic with a trivial translation. Therefore the terms are often used interchangeably. --Stephan Schulz (talk) 01:44, 20 June 2008 (UTC)[reply]

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)[reply]