mathematical logic Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...

, a formula is in negation normal form (NNF) if the

negation In logic, negation, also called the logical not or logical complement, is an operation (mathematics), operation that takes a Proposition (mathematics), proposition P to another proposition "not P", written \neg P, \mathord P, P^\prime or \over ...

operator (

\lnot

, ) is only applied to variables and the only other allowed Boolean operators are conjunction (

\land

, ) and

disjunction In logic, disjunction (also known as logical disjunction, logical or, logical addition, or inclusive disjunction) is a logical connective typically notated as \lor and read aloud as "or". For instance, the English language sentence "it is ...

(

\lor

, ). Negation normal form is not a

canonical form In mathematics and computer science, a canonical, normal, or standard form of a mathematical object is a standard way of presenting that object as a mathematical expression. Often, it is one which provides the simplest representation of an obje ...

: for example,

a \land (b\lor \lnot c)

and

(a \land b) \lor (a \land \lnot c)

are equivalent, and are both in negation normal form.

Definition

The following is a

context-free grammar In formal language theory, a context-free grammar (CFG) is a formal grammar whose production rules can be applied to a nonterminal symbol regardless of its context. In particular, in a context-free grammar, each production rule is of the fo ...

for ''NNF'': : where ''Variable'' is any variable.

Examples and counterexamples

: The following formulae are all in negation normal form: :

\begin
&((A \lor B) \land C) \\
&(A \lor \lnot B) \\
&(A \land \lnot B) \\
&\
\end

The first example is also in

conjunctive normal form In Boolean algebra, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is a product of sums or an AND of ORs. In au ...

, the next two are in both

and

disjunctive normal form In boolean logic, a disjunctive normal form (DNF) is a canonical normal form of a logical formula consisting of a disjunction of conjunctions; it can also be described as an OR of ANDs, a sum of products, or in philosophical logic a ''cluster c ...

, but the last example is in neither. The following formulae are not in negation normal form: :

\begin
         (A &\to B) \\
  \lnot (A &\lor B) \\
  \lnot (A &\land B) \\
  \lnot (A &\lor \lnot C)
\end

They are however respectively equivalent to the following formulae in negation normal form: :

\begin
  (\lnot A &\lor B) \\
  (\lnot A &\land \lnot B) \\
  (\lnot A &\lor \lnot B) \\
  (\lnot A &\land C)
\end

Conversion to NNF

classical logic Classical logic (or standard logic) or Frege–Russell logic is the intensively studied and most widely used class of deductive logic. Classical logic has had much influence on analytic philosophy. Characteristics Each logical system in this c ...

and many

modal logic Modal logic is a kind of logic used to represent statements about Modality (natural language), necessity and possibility. In philosophy and related fields it is used as a tool for understanding concepts such as knowledge, obligation, and causality ...

s, every formula can be brought into this form by replacing implications (

\to

) and equivalences (

\leftrightarrow

) by their definitions, using

De Morgan's laws In propositional calculus, propositional logic and Boolean algebra, De Morgan's laws, also known as De Morgan's theorem, are a pair of transformation rules that are both Validity (logic), valid rule of inference, rules of inference. They are nam ...

to push negation inwards, and eliminating double negations. This process can be represented using the following rewrite rules: :

\begin
    A \to B &~\rightsquigarrow~ \lnot A \lor B \\
    A \leftrightarrow B &~\rightsquigarrow~ (\lnot A \lor B) \land (A \lor \lnot B) \\
   \lnot (A \lor B) &~\rightsquigarrow~ \lnot A \land \lnot B \\
  \lnot (A \land B) &~\rightsquigarrow~ \lnot A \lor \lnot B \\
      \lnot \lnot A &~\rightsquigarrow~ A \\
  \lnot \exists x A &~\rightsquigarrow~ \forall x \lnot A \\
  \lnot \forall x A &~\rightsquigarrow~ \exists x \lnot A
\end

Transformation into negation normal form can increase the size of a formula only linearly: the number of occurrences of atomic formulas remains the same, the total number of occurrences of

\land

and

\lor

is unchanged, and the number of occurrences of

\lnot

in the normal form is bounded by the length of the original formula. A formula in negation normal form can be put into the stronger

by applying

distributivity In mathematics, the distributive property of binary operations is a generalization of the distributive law, which asserts that the equality x \cdot (y + z) = x \cdot y + x \cdot z is always true in elementary algebra. For example, in elementary ...

. Repeated application of distributivity may exponentially increase the size of a formula. In the classical

propositional logic The propositional calculus is a branch of logic. It is also called propositional logic, statement logic, sentential calculus, sentential logic, or sometimes zeroth-order logic. Sometimes, it is called ''first-order'' propositional logic to contra ...

, transformation to negation normal form does not impact computational properties: the satisfiability problem continues to be

NP-complete In computational complexity theory, NP-complete problems are the hardest of the problems to which ''solutions'' can be verified ''quickly''. Somewhat more precisely, a problem is NP-complete when: # It is a decision problem, meaning that for any ...

, and the validity problem continues to be

co-NP-complete In complexity theory, computational problems that are co-NP-complete are those that are the hardest problems in co-NP, in the sense that any problem in co-NP can be reformulated as a special case of any co-NP-complete problem with only polynomial ...

. For formulas in conjunctive normal form, the validity problem is solvable in polynomial time, and for formulas in disjunctive normal form, the satisfiability problem is solvable in polynomial time.

Notes

References

External links