Talk:Clausal normal form

From Wikipedia, the free encyclopedia
Jump to: navigation, search
WikiProject Mathematics (Rated Stub-class, Low-priority)
WikiProject Mathematics
This redirect is within the scope of WikiProject Mathematics, a collaborative effort to improve the coverage of Mathematics on Wikipedia. If you would like to participate, please visit the project page, where you can join the discussion and see a list of open tasks.
Mathematics rating:
Stub Class
Low Priority
 Field:  Foundations, logic, and set theory

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. (talk) 14:22, 1 June 2008 (UTC)

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.) (talk) 14:43, 1 June 2008 (UTC)

Shouldn't this page be merged with Conjunctive Normal Form? (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)
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)
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)