Normal conjunctive form

In propositional logic, a certain form of formulas is referred to as the conjunctive normal form ( KNF for short , CNF for conjunctive normal form ) .

definition

A propositional logic formula is in conjunctive normal form if it is a conjunction of disjunction terms . Disjunction terms are disjunctions of literals . Literals are non-negated or negated variables. So a formula in KNF has the form

${\displaystyle \bigwedge _{i}\bigvee _{j}(\neg )x_{ij}.}$

Example:

${\displaystyle (A\vee B\vee C)\wedge ({\bar {A}}\vee B\vee C)}$

Canonical conjunctive normal form

A canonical conjunctive normal form (KKNF) consists of pairwise different maxterms . Each variable occurs exactly once in each of these maxterms. Each Boolean function has exactly one KKNF. The KKNF is also called the complete conjunctive normal form .

education

Every formula of propositional logic can be converted into conjunctive normal form, since every Boolean function can also be represented with a CNF. All you have to do is read the lines of your truth table . For each line that returns a 0 as a result, a clause is formed that disjunctively links all variables of the function with the inverted assignment. The resulting terms are max terms. Their conjunctive connection is provided by the canonical conjunctive normal form.

As a rule, this is not a minimal formula, i.e. a formula with as few clauses as possible. If you want to create a minimal formula, you can do this with the help of Karnaugh-Veitch diagrams (KV diagrams for short).

The Quine and McCluskey method can be used to calculate the conjunctive normal form of any formula. To do this, the formula is negated, then transformed into the disjunctive normal form using the Quine and McCluskey method and then negated again.

Example of education

We are looking for a formula in CNF for the Boolean function with three variables x ₂ , x ₁ and x ₀ , which assumes the truth value 1 (true) if and only if the binary number [ x ₂ x ₁ x ₀ ] _{2 is} a prime number .

The truth table for this function has the following form:

Note: The individual clauses are noted as maxterms . The figure also shows that every KNF has an equivalent DNF .

Decidability

The question of whether the variables of a propositional formula can be documented in such a way that the proposition becomes true is called the satisfiability problem ( SAT for short ). SAT belongs to the class of NP-complete problems and is therefore generally considered to be difficult to solve. This also applies to formulas that are available in KNF; Horn formulas , which represent a special case of the CNF formulas and can be tested for satisfiability in polynomial time , are an exception . There are basically two approaches how a propositional expression can be checked for its satisfiability: by testing all possible assignments of its variables (semantic approach) or by using the resolution calculus (purely syntactically).

More normal forms

In addition to the conjunctive normal form, there are other normal forms in propositional logic , such as the disjunctive normal form , the negation normal form or the canonical normal form .

Individual evidence

1. ↑ In some sources (e.g. Klaus Beuth: Digitaltechnik , ISBN 9783802319587 , on p. 78), the CNF is precisely this canonical CNF.

Web links

• Web form for conversion into the "normal conjunctive form"