Conjunctive normal form

As described above, the resolution rule applies only to literal clauses, so at first glance it applies only to knowledge bases and queries consisting of such clauses. On what basis do we argue that this rule can serve as the basis for a complete logical inference procedure for all propositional logic? The answer to this question is that each statement of propositional logic is logically equivalent to a conjunction of disjunctions of literals .

Any statement presented as a conjunction of literal disjunctions is called a conjunctive normal form , or CNF (Conjunctive Normal Form). In addition, it will be shown below that it is also advisable to define a limited family of statements in conjunctive normal form, called sentences in the form of k-CNF . The statement in the form of k-CNF has exactly 7c literals per expression:

(l _1,1 v ... vl _{1, k} ) ^ ... ^ (l _{n, 1} v ... vl _{n, k} )

As it turned out, any statement can be transformed into a 3-CNF statement, which has an equivalent set of models. Instead of proving these statements, we describe a simple transformation procedure. We illustrate this procedure by transforming R ₂ , or B _1.1 <=> (P _1,2 vP _2,1 ), into the form CNF. The following steps describe the relevant steps.

1. Eliminate the link <=>, replacing the statement α <=> β with the statement (α => β) ^ (β <=> α): (B _1,1 => (P _1,2 v P _2,1 )) ^ ( (P _1,2 v P _2,1 ) => B _1,1 )
2. Eliminate the link =>, replacing the statement α => β with the phrase ¬α v β: (¬B _1,1 v P _1,2 v P _2,1 ) ^ (¬ (P _1,2 v P _2,1 ) v B _1,1 )
3. The conjunctive normal form requires that the bundle ¬ appear only before the literals, therefore, as it is called this operation, "we will introduce the bundle ¬ inside the expression", repeating the operation of applying the following equivalences from the listing
4. The result is a statement containing nested bundles ^ and v, which are applied to literals. We use the law of distributivity, shown in the listing, distributing bundles of v across bundles of l wherever possible.

Now the original statement is presented in the form of CNF, as a conjunction of three expressions. This statement has become more difficult to read, but it can be used as input to the resolution procedure.