![Disjunctive normal form](https://www.english.nina.az/wikipedia/image/aHR0cHM6Ly91cGxvYWQud2lraW1lZGlhLm9yZy93aWtpcGVkaWEvY29tbW9ucy90aHVtYi8wLzBjL0thcm5hdWdoX21hcF9LVl80bWFsNF8xOC5zdmcvMTYwMHB4LUthcm5hdWdoX21hcF9LVl80bWFsNF8xOC5zdmcucG5n.png )
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 concept. As a normal form, it is useful in automated theorem proving.
Definition
A logical formula is considered to be in DNF if it is a disjunction of one or more conjunctions of one or more literals. A DNF formula is in full disjunctive normal form if each of its variables appears exactly once in every conjunction and each conjunction appears at most once (up to the order of variables). As in conjunctive normal form (CNF), the only propositional operators in DNF are and (), or (
), and not (
). The not operator can only be used as part of a literal, which means that it can only precede a propositional variable.
The following is a context-free grammar for DNF:
- DNF → (Conjunction)
DNF
- DNF → (Conjunction)
- Conjunction → Literal
Conjunction
- Conjunction → Literal
- Literal →
Variable
- Literal → Variable
Where Variable is any variable.
For example, all of the following formulas are in DNF:
The formula is in DNF, but not in full DNF; an equivalent full-DNF version is
.
The following formulas are not in DNF:
, since an OR is nested within a NOT
, since an AND is nested within a NOT
, since an OR is nested within an AND
Conversion to DNF
In classical logic each propositional formula can be converted to DNF ...
![image](https://www.english.nina.az/wikipedia/image/aHR0cHM6Ly93d3cuZW5nbGlzaC5uaW5hLmF6L3dpa2lwZWRpYS9pbWFnZS9hSFIwY0hNNkx5OTFjR3h2WVdRdWQybHJhVzFsWkdsaExtOXlaeTkzYVd0cGNHVmthV0V2WTI5dGJXOXVjeTkwYUhWdFlpOHdMekJqTDB0aGNtNWhkV2RvWDIxaGNGOUxWbDgwYldGc05GOHhPQzV6ZG1jdk1qSXdjSGd0UzJGeWJtRjFaMmhmYldGd1gwdFdYelJ0WVd3MFh6RTRMbk4yWnk1d2JtYz0ucG5n.png)
![image](https://www.english.nina.az/wikipedia/image/aHR0cHM6Ly93d3cuZW5nbGlzaC5uaW5hLmF6L3dpa2lwZWRpYS9pbWFnZS9hSFIwY0hNNkx5OTFjR3h2WVdRdWQybHJhVzFsWkdsaExtOXlaeTkzYVd0cGNHVmthV0V2WTI5dGJXOXVjeTkwYUhWdFlpOWtMMlEwTDB0aGNtNWhkV2RvWDIxaGNGOUxWbDgwYldGc05GOHhPUzV6ZG1jdk1qSXdjSGd0UzJGeWJtRjFaMmhmYldGd1gwdFdYelJ0WVd3MFh6RTVMbk4yWnk1d2JtYz0ucG5n.png)
... by syntactic means
The conversion involves using logical equivalences, such as double negation elimination, De Morgan's laws, and the distributive law. Formulas built from the primitive connectives can be converted to DNF by the following canonical term rewriting system:
... by semantic means
The full DNF of a formula can be read off its truth table. For example, consider the formula
.
The corresponding truth table is
T T T F T F F T F T T F F T F T T F T F T T F T F T T T F F T F F T F T F T T T F T F T T F T F T F F T F T F F T T F T F T F F F F T F T T T F
- The full DNF equivalent of
is
- The full DNF equivalent of
is
Remark
A propositional formula can be represented by one and only one full DNF. In contrast, several plain DNFs may be possible. For example, by applying the rule three times, the full DNF of the above
can be simplified to
. However, there are also equivalent DNF formulas that cannot be transformed one into another by this rule, see the pictures for an example.
Disjunctive Normal Form Theorem
It is a theorem that all consistent formulas in propositional logic can be converted to disjunctive normal form. This is called the Disjunctive Normal Form Theorem. The formal statement is as follows:
Disjunctive Normal Form Theorem: Suppose
is a sentence in a propositional language
with
sentence letters, which we shall denote by
. If
is not a contradiction, then it is truth-functionally equivalent to a disjunction of conjunctions of the form
, where
, and
.
The proof follows from the procedure given above for generating DNFs from truth tables. Formally, the proof is as follows:
Suppose
is a sentence in a propositional language whose sentence letters are
. For each row of
's truth table, write out a corresponding conjunction
, where
is defined to be
if
takes the value
at that row, and is
if
takes the value
at that row; similarly for
,
, etc. (the alphabetical ordering of
in the conjunctions is quite arbitrary; any other could be chosen instead). Now form the disjunction of all these conjunctions which correspond to
rows of
's truth table. This disjunction is a sentence in
, which by the reasoning above is truth-functionally equivalent to
. This construction obviously presupposes that
takes the value
on at least one row of its truth table; if
doesn’t, i.e., if
is a contradiction, then
is equivalent to
, which is, of course, also a sentence in
.
This theorem is a convenient way to derive many useful metalogical results in propositional logic, such as, trivially, the result that the set of connectives is functionally complete.
Maximum number of conjunctions
Any propositional formula is built from variables, where
.
There are possible literals:
.
has
non-empty subsets.
This is the maximum number of conjunctions a DNF can have.
A full DNF can have up to conjunctions, one for each row of the truth table.
Example 1
Consider a formula with two variables and
.
The longest possible DNF has conjunctions:
The longest possible full DNF has 4 conjunctions: they are underlined.
This formula is a tautology.
Example 2
Each DNF of the e.g. formula has
conjunctions.
Computational complexity
The Boolean satisfiability problem on conjunctive normal form formulas is NP-complete. By the duality principle, so is the falsifiability problem on DNF formulas. Therefore, it is co-NP-hard to decide if a DNF formula is a tautology.
Conversely, a DNF formula is satisfiable if, and only if, one of its conjunctions is satisfiable. This can be decided in polynomial time simply by checking that at least one conjunction does not contain conflicting literals.
Variants
An important variation used in the study of computational complexity is k-DNF. A formula is in k-DNF if it is in DNF and each conjunction contains at most k literals.
See also
- Algebraic normal form – an XOR of AND clauses
- Blake canonical form – DNF including all prime implicants
- Quine–McCluskey algorithm – algorithm for calculating prime implicants
- Conjunction/disjunction duality
- Propositional logic
- Truth table
Notes
- Post 1921.
- Davey & Priestley 1990, p. 153.
- Gries & Schneider 1993, p. 67.
- Whitesitt 2012, pp. 33–37.
- However, this one is in negation normal form.
- Davey & Priestley 1990, p. 152-153.
- Formulas with other connectives can be brought into negation normal form first.
- Dershowitz & Jouannaud 1990, p. 270, Sect.5.1.
- Sobolev 2020.
-
= ((NOT (p AND q)) IFF ((NOT r) NAND (p XOR q)))
- like
- It is assumed that repetitions and variations based on the commutativity and associativity of
and
do not occur.
- Halbeisen, Lorenz; Kraph, Regula (2020). Gödel´s theorems and zermelo´s axioms: a firm foundation of mathematics. Cham: Birkhäuser. p. 27. ISBN 978-3-030-52279-7.
- Howson, Colin (1997). Logic with trees: an introduction to symbolic logic. London; New York: Routledge. p. 41. ISBN 978-0-415-13342-5.
- Cenzer, Douglas; Larson, Jean; Porter, Christopher; Zapletal, Jindřich (2020). Set theory and foundations of mathematics: an introduction to mathematical logic. New Jersey: World Scientific. pp. 19–21. ISBN 978-981-12-0192-9.
- Halvorson, Hans (2020). How logic works: a user's guide. Princeton Oxford: Princeton University Press. p. 195. ISBN 978-0-691-18222-3.
- That is, the language with the propositional variables
and the connectives
.
-
- Arora & Barak 2009.
References
- Arora, Sanjeev; Barak, Boaz (20 April 2009). Computational Complexity: A Modern Approach. Cambridge University Press. p. 579. doi:10.1017/CBO9780511804090. ISBN 9780521424264.
- Davey, B.A.; Priestley, H.A. (1990). Introduction to Lattices and Order. Cambridge Mathematical Textbooks. Cambridge University Press.
- Dershowitz, Nachum; Jouannaud, Jean-Pierre (1990). "Rewrite Systems". In Van Leeuwen, Jan (ed.). Formal Models and Semantics. Handbook of Theoretical Computer Science. Vol. B. Elsevier. pp. 243–320. ISBN 0-444-88074-7.
- Gries, David; Schneider, Fred B. (22 October 1993). A Logical Approach to Discrete Math. Springer Science & Business Media. ISBN 978-0-387-94115-8.
- Hilbert, David; Ackermann, Wilhelm (1999). Principles of Mathematical Logic. American Mathematical Soc. ISBN 978-0-8218-2024-7.
- Howson, Colin (11 October 2005) [1997]. Logic with trees: an introduction to symbolic logic. Routledge. ISBN 978-1-134-78550-6.
- Post, Emil (July 1921). "Introduction to a General Theory of Elementary Propositions". American Journal of Mathematics. 43 (3): 163–185. doi:10.2307/2370324. JSTOR 2370324.
- Sobolev, S.K. (2020) [1994], "Disjunctive normal form", Encyclopedia of Mathematics, EMS Press
- Whitesitt, J. Eldon (24 May 2012) [1961]. Boolean Algebra and Its Applications. Courier Corporation. ISBN 978-0-486-15816-7.
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 concept As a normal form it is useful in automated theorem proving DefinitionA logical formula is considered to be in DNF if it is a disjunction of one or more conjunctions of one or more literals A DNF formula is in full disjunctive normal form if each of its variables appears exactly once in every conjunction and each conjunction appears at most once up to the order of variables As in conjunctive normal form CNF the only propositional operators in DNF are and displaystyle wedge or displaystyle vee and not displaystyle neg The not operator can only be used as part of a literal which means that it can only precede a propositional variable The following is a context free grammar for DNF DNF Conjunction displaystyle vee DNF DNF Conjunction Conjunction Literal displaystyle wedge Conjunction Conjunction Literal Literal displaystyle neg Variable Literal Variable Where Variable is any variable For example all of the following formulas are in DNF A B C D E F D F displaystyle A land neg B land neg C lor neg D land E land F land D land F A B C displaystyle A land B lor C A B displaystyle A land B A displaystyle A The formula A B displaystyle A lor B is in DNF but not in full DNF an equivalent full DNF version is A B A B A B displaystyle A land B lor A land lnot B lor lnot A land B The following formulas are not in DNF A B displaystyle neg A lor B since an OR is nested within a NOT A B C displaystyle neg A land B lor C since an AND is nested within a NOT A B C D displaystyle A lor B land C lor D since an OR is nested within an ANDConversion to DNFIn classical logic each propositional formula can be converted to DNF Karnaugh map of the disjunctive normal form A B D A B C A B D A B C Karnaugh map of the disjunctive normal form A C D B C D A C D B C D Despite the different grouping the same fields contain a 1 as in the previous map by syntactic means The conversion involves using logical equivalences such as double negation elimination De Morgan s laws and the distributive law Formulas built from the primitive connectives displaystyle land lor lnot can be converted to DNF by the following canonical term rewriting system x x x y x y x y x y x y z x y x z x y z x z y z displaystyle begin array rcl lnot lnot x amp rightsquigarrow amp x lnot x lor y amp rightsquigarrow amp lnot x land lnot y lnot x land y amp rightsquigarrow amp lnot x lor lnot y x land y lor z amp rightsquigarrow amp x land y lor x land z x lor y land z amp rightsquigarrow amp x land z lor y land z end array by semantic means The full DNF of a formula can be read off its truth table For example consider the formula ϕ p q r p q displaystyle phi lnot p land q leftrightarrow lnot r uparrow p oplus q The corresponding truth table is p displaystyle p q displaystyle q r displaystyle r displaystyle displaystyle lnot p q displaystyle p land q displaystyle displaystyle leftrightarrow displaystyle r displaystyle lnot r displaystyle uparrow p q displaystyle p oplus q displaystyle T T T F T F F T FT T F F T F T T FT F T T F T F T TT F F T F F T F TF T T T F T F T TF T F T F F T F TF F T T F T F T FF F F T F T T T FThe full DNF equivalent of ϕ displaystyle phi is p q r p q r p q r p q r displaystyle p land lnot q land r lor lnot p land q land r lor lnot p land lnot q land r lor lnot p land lnot q land lnot r The full DNF equivalent of ϕ displaystyle lnot phi is p q r p q r p q r p q r displaystyle p land q land r lor p land q land lnot r lor p land lnot q land lnot r lor lnot p land q land lnot r Remark A propositional formula can be represented by one and only one full DNF In contrast several plain DNFs may be possible For example by applying the rule a b a b b displaystyle a land b lor lnot a land b rightsquigarrow b three times the full DNF of the above ϕ displaystyle phi can be simplified to p q p r q r displaystyle lnot p land lnot q lor lnot p land r lor lnot q land r However there are also equivalent DNF formulas that cannot be transformed one into another by this rule see the pictures for an example Disjunctive Normal Form TheoremIt is a theorem that all consistent formulas in propositional logic can be converted to disjunctive normal form This is called the Disjunctive Normal Form Theorem The formal statement is as follows Disjunctive Normal Form Theorem Suppose X displaystyle X is a sentence in a propositional language L displaystyle mathcal L with n displaystyle n sentence letters which we shall denote by A1 An displaystyle A 1 A n If X displaystyle X is not a contradiction then it is truth functionally equivalent to a disjunction of conjunctions of the form A1 An displaystyle pm A 1 land land pm A n where Ai Ai displaystyle A i A i and Ai Ai displaystyle A i neg A i The proof follows from the procedure given above for generating DNFs from truth tables Formally the proof is as follows Suppose X displaystyle X is a sentence in a propositional language whose sentence letters are A B C displaystyle A B C ldots For each row of X displaystyle X s truth table write out a corresponding conjunction A B C displaystyle pm A land pm B land pm C land ldots where A displaystyle pm A is defined to be A displaystyle A if A displaystyle A takes the value T displaystyle T at that row and is A displaystyle neg A if A displaystyle A takes the value F displaystyle F at that row similarly for B displaystyle pm B C displaystyle pm C etc the alphabetical ordering of A B C displaystyle A B C ldots in the conjunctions is quite arbitrary any other could be chosen instead Now form the disjunction of all these conjunctions which correspond to T displaystyle T rows of X displaystyle X s truth table This disjunction is a sentence in L A B C displaystyle mathcal L A B C ldots land lor neg which by the reasoning above is truth functionally equivalent to X displaystyle X This construction obviously presupposes that X displaystyle X takes the value T displaystyle T on at least one row of its truth table if X displaystyle X doesn t i e if X displaystyle X is a contradiction then X displaystyle X is equivalent to A A displaystyle A land neg A which is of course also a sentence in L A B C displaystyle mathcal L A B C ldots land lor neg This theorem is a convenient way to derive many useful metalogical results in propositional logic such as trivially the result that the set of connectives displaystyle land lor neg is functionally complete Maximum number of conjunctionsAny propositional formula is built from n displaystyle n variables where n 1 displaystyle n geq 1 There are 2n displaystyle 2n possible literals L p1 p1 p2 p2 pn pn displaystyle L p 1 lnot p 1 p 2 lnot p 2 ldots p n lnot p n L displaystyle L has 22n 1 displaystyle 2 2n 1 non empty subsets This is the maximum number of conjunctions a DNF can have A full DNF can have up to 2n displaystyle 2 n conjunctions one for each row of the truth table Example 1 Consider a formula with two variables p displaystyle p and q displaystyle q The longest possible DNF has 2 2 2 1 15 displaystyle 2 2 times 2 1 15 conjunctions p p q q p p p q p q p q p q q q p p q p p q p q q p q q p p q q displaystyle begin array lcl lnot p lor p lor lnot q lor q lor lnot p land p lor underline lnot p land lnot q lor underline lnot p land q lor underline p land lnot q lor underline p land q lor lnot q land q lor lnot p land p land lnot q lor lnot p land p land q lor lnot p land lnot q land q lor p land lnot q land q lor lnot p land p land lnot q land q end array The longest possible full DNF has 4 conjunctions they are underlined This formula is a tautology Example 2 Each DNF of the e g formula X1 Y1 X2 Y2 Xn Yn displaystyle X 1 lor Y 1 land X 2 lor Y 2 land dots land X n lor Y n has 2n displaystyle 2 n conjunctions Computational complexityThe Boolean satisfiability problem on conjunctive normal form formulas is NP complete By the duality principle so is the falsifiability problem on DNF formulas Therefore it is co NP hard to decide if a DNF formula is a tautology Conversely a DNF formula is satisfiable if and only if one of its conjunctions is satisfiable This can be decided in polynomial time simply by checking that at least one conjunction does not contain conflicting literals VariantsAn important variation used in the study of computational complexity is k DNF A formula is in k DNF if it is in DNF and each conjunction contains at most k literals See alsoAlgebraic normal form an XOR of AND clauses Blake canonical form DNF including all prime implicants Quine McCluskey algorithm algorithm for calculating prime implicants Conjunction disjunction duality Propositional logic Truth tableNotesPost 1921 Davey amp Priestley 1990 p 153 Gries amp Schneider 1993 p 67 Whitesitt 2012 pp 33 37 However this one is in negation normal form Davey amp Priestley 1990 p 152 153 Formulas with other connectives can be brought into negation normal form first Dershowitz amp Jouannaud 1990 p 270 Sect 5 1 Sobolev 2020 ϕ displaystyle phi NOT p AND q IFF NOT r NAND p XOR q like a b b a a b b displaystyle a land b lor b land a lor a land b land b It is assumed that repetitions and variations based on the commutativity and associativity of displaystyle lor and displaystyle land do not occur Halbeisen Lorenz Kraph Regula 2020 Godel s theorems and zermelo s axioms a firm foundation of mathematics Cham Birkhauser p 27 ISBN 978 3 030 52279 7 Howson Colin 1997 Logic with trees an introduction to symbolic logic London New York Routledge p 41 ISBN 978 0 415 13342 5 Cenzer Douglas Larson Jean Porter Christopher Zapletal Jindrich 2020 Set theory and foundations of mathematics an introduction to mathematical logic New Jersey World Scientific pp 19 21 ISBN 978 981 12 0192 9 Halvorson Hans 2020 How logic works a user s guide Princeton Oxford Princeton University Press p 195 ISBN 978 0 691 18222 3 That is the language with the propositional variables A B C displaystyle A B C ldots and the connectives displaystyle land lor neg P L 22n displaystyle left mathcal P L right 2 2n Arora amp Barak 2009 ReferencesArora Sanjeev Barak Boaz 20 April 2009 Computational Complexity A Modern Approach Cambridge University Press p 579 doi 10 1017 CBO9780511804090 ISBN 9780521424264 Davey B A Priestley H A 1990 Introduction to Lattices and Order Cambridge Mathematical Textbooks Cambridge University Press Dershowitz Nachum Jouannaud Jean Pierre 1990 Rewrite Systems In Van Leeuwen Jan ed Formal Models and Semantics Handbook of Theoretical Computer Science Vol B Elsevier pp 243 320 ISBN 0 444 88074 7 Gries David Schneider Fred B 22 October 1993 A Logical Approach to Discrete Math Springer Science amp Business Media ISBN 978 0 387 94115 8 Hilbert David Ackermann Wilhelm 1999 Principles of Mathematical Logic American Mathematical Soc ISBN 978 0 8218 2024 7 Howson Colin 11 October 2005 1997 Logic with trees an introduction to symbolic logic Routledge ISBN 978 1 134 78550 6 Post Emil July 1921 Introduction to a General Theory of Elementary Propositions American Journal of Mathematics 43 3 163 185 doi 10 2307 2370324 JSTOR 2370324 Sobolev S K 2020 1994 Disjunctive normal form Encyclopedia of Mathematics EMS Press Whitesitt J Eldon 24 May 2012 1961 Boolean Algebra and Its Applications Courier Corporation ISBN 978 0 486 15816 7