Conjunctive Normal Form -artificial intelligence :
For the resolution law to determine two sentences, they should both be in a normalized format known as conjunctive normal form, which is generally cut to CNF. This is an unlucky name because the sentences themselves are made up of orders of disjunctions. It is implicitly understood that the whole knowledge base is a huge conjunction of the sentences, which is where conjunctive normal form haveits name. So, CNF is basically a conjunction of disjunctions. The disjunctions are made up of literals which may either be a predicate or the negation of a predicate (for propositional read a proposition or the negation of a proposition):
So, CNF sentences are of the form:
(p1∨p2 ∨ ... ∨ pm) ∧ (q1 ∨ q2 ∨ ...∨qn)∧ etc.
Where each pi and qj is a truthful. Note that we call the disjunction of such truthful a Clause. As a concrete example,
Likes (George, X) ∨ likes (tony, George)∨¬ is mad(Maggie)
Is in conjunctive normal form, but:
Likes (George, X) ∨ likes (tony, George) -> ¬ is mad (Maggie) ∧ is mad (tony) is not in CNF.
The following eight-stage method converts any sentence into CNF:
1. remove arrow connectives by rewriting with
P <-> Q => (P ->Q) ∧(Q ->P)
P<-> Q => ¬P ∨ Q
2. Move ¬ inwards using De Morgan's laws (inc. quantifier versions) and double negation:
¬ (P ∨ Q) => ¬P ∧ Q
¬ (P ∧ Q) => ¬P ∨ Q
¬ ∀X. P => X. ¬P
¬∃X. P => X. ¬P
¬¬P => P
3. Rename variables distant: the similar variable name may be reused a lot of time for different variables, within one sentence or among several. To ignore uncertainty later rename every dissimilar variable with a exclusive name.
4. Move quantifiers outwards: the sentence is now in a form where all the quantifiers may be moved strongly to the outside without disturbing the semantics, provided they are reserved in the similar order.
5. Solemnize existential variables by replacing them with Solemn constants and methods. This is similar to the existential removal law from the last format we just replace a word for each existential variable so as to represents the 'something' for which it handles. If there are no preceding unique quantifiers the 'something' is immediately a new constant. However, if there are then we use a method that may have all these preceding unique variables as arguments. When we are done we immediately drop all the general quantifiers. This leaves a quantifier-free statement . For example:
∀X. ∃Y. person(X)-> has(X, Y) ∧heart(Y) is Solemnized like
person (X) ->has(X, f(X)) ∧heart(f(X))
6. Distribut ∧ over ∨ to get a conjunction of disjunctions. This includes rewriting with:
P ∧(Q ∨R) => (P ∧Q) ∨(P ∧R)
(P∨Q)∧ R => (P∧R) (Q ∧ R)
7. Flatten binary connectives: swap nested ∧ and ∨ with flat lists of conjuncts and disjoints:
P ∧(Q∧ R) => P∧ Q ∧ R
(P∧ Q)∧ R => P ∧ Q∧ R
P ∨ (Q ∨ R) => P∨Q∨R
(P ∨ Q) ∨ R => P ∨ Q ∨ R
8. The sentence is now in CNF. more simplification may take place by avoiding duplicate literals and sinking any clause which contains both A and ¬A (one will be right, so the clause is always right. In the conjunction of clauses we need everything to be exact, so we can drop it.) There is an another possible final step that takes it to Kowalski normal form, also famous as implicative normal form (INF):
9. Reintroduce implication by collecting up all the negative literals (the negated ones) and making their conjunction N, then taking the disjunction P of the affirmative literals, and forming the logically equivalent clause N-> P.