This article needs additional citations for verification. (July 2013) (Learn how and when to remove this template message)
- The entire formula is purely true or false:
- One or more variables are ANDed together into a term, then one or more terms are XORed together into ANF. No NOTs are permitted:
- a ⊕ b ⊕ ab ⊕ abc
- or in standard propositional logic symbols:
- The previous subform with a purely true term:
- 1 ⊕ a ⊕ b ⊕ ab ⊕ abc
ANF is a normal form, which means that two equivalent formulas will convert to the same ANF, easily showing whether two formulas are equivalent for automated theorem proving. Unlike other normal forms, it can be represented as a simple list of lists of variable names. Conjunctive and disjunctive normal forms also require recording whether each variable is negated or not. Negation normal form is unsuitable for that purpose, since it doesn't use equality as its equivalence relation: a ∨ ¬a isn't reduced to the same thing as 1, even though they're equal.
Putting a formula into ANF also makes it easy to identify linear functions (used, for example, in linear feedback shift registers): a linear function is one that is a sum of single literals. Properties of nonlinear feedback shift registers can also be deduced from certain properties of the feedback function in ANF.
Performing operations within algebraic normal form
There are straightforward ways to perform the standard boolean operations on ANF inputs in order to get ANF results.
XOR (logical exclusive disjunction) is performed directly:
- (1 ⊕ x) ⊕ (1 ⊕ x ⊕ y)
- 1 ⊕ x ⊕ 1 ⊕ x ⊕ y
- 1 ⊕ 1 ⊕ x ⊕ x ⊕ y
NOT (logical negation) is XORing 1:
- ¬(1 ⊕ x ⊕ y)
- 1 ⊕(1 ⊕ x ⊕ y)
- 1 ⊕ 1 ⊕ x ⊕ y
- x ⊕ y
- (1 ⊕ x)(1 ⊕ x ⊕ y)
- 1(1 ⊕ x ⊕ y) ⊕ x(1 ⊕ x ⊕ y)
- (1 ⊕ x ⊕ y) ⊕ (x ⊕ x ⊕ xy)
- 1 ⊕ x ⊕ x ⊕ x ⊕ y ⊕ xy
- 1 ⊕ x ⊕ y ⊕ xy
- (1 ⊕ x) + (1 ⊕ x ⊕ y)
- 1 ⊕ (1 ⊕ 1 ⊕ x)(1 ⊕ 1 ⊕ x ⊕ y)
- 1 ⊕ x(x ⊕ y)
- 1 ⊕ x ⊕ xy
Converting to algebraic normal form
Each variable in a formula is already in pure ANF, so you only need to perform the formula's boolean operations as shown above to get the entire formula into ANF. For example:
- x + (y · ¬z)
- x + (y(1 ⊕ z))
- x + (y ⊕ yz)
- x ⊕ (y ⊕ yz) ⊕ x(y ⊕ yz)
- x ⊕ y ⊕ xy ⊕ yz ⊕ xyz
ANF is sometimes described in an equivalent way:
- where fully describes .
Recursively deriving multiargument Boolean functions
There are only four functions with one argument:
To represent a function with multiple arguments one can use the following equality:
- , where
- if then and so
- if then and so
Since both and have fewer arguments than it follows that using this process recursively we will finish with functions with one variable. For example, let us construct ANF of (logical or):
- since and
- it follows that
- by distribution, we get the final ANF:
- Reed–Muller expansion
- Zhegalkin normal form
- Boolean function
- Logical graph
- Zhegalkin polynomial
- Negation normal form
- Conjunctive normal form
- Disjunctive normal form
- Karnaugh map
- Boolean ring
- Steinbach, Bernd; Posthoff, Christian (2009). "Preface". Logic Functions and Equations - Examples and Exercises (1st ed.). Springer Science + Business Media B. V. p. xv. ISBN 978-1-4020-9594-8. LCCN 2008941076.
- WolframAlpha NOT-equivalence demonstration: ¬a = 1 ⊕ a
- WolframAlpha AND-equivalence demonstration: (a ⊕ b)(c ⊕ d) = ac ⊕ ad ⊕ bc ⊕ bd
- From De Morgan's laws
- WolframAlpha OR-equivalence demonstration: a + b = a ⊕ b ⊕ ab
- Wegener, Ingo (1987). The complexity of Boolean functions. Wiley-Teubner. p. 6. ISBN 3-519-02107-2.
- "Presentation" (PDF) (in German). University of Duisburg-Essen. Archived (PDF) from the original on 2017-04-19. Retrieved 2017-04-19.
- Maxfield, Clive "Max" (2006-11-29). "Reed-Muller Logic". Logic 101. EETimes. Part 3. Archived from the original on 2017-04-19. Retrieved 2017-04-19.