The over-bar notation x is used equivalently with ¬x for the Boolean negation operator. First some definitions are introduced. A Boolean proposition is a statement that can be true or false (1 or 0). For example “It is raining” or “the street is wet” are two statements that can be true or false. Let x and y be two Boolean propositions. A negated or un-negated proposition is called literal (for example: x or y). An expression formed of literals and an and operator is called conjunction. An expression formed of literals and an or operator is called disjunction. A clause is a – possibly empty – disjunction of literals. The following two expressions are examples of clauses :

A Horn-clause is a clause with at most one un-negated literal. Above, the first clause is a Horn-clause while the second is not. A conjunctive normal form (CNF) is a formula which is a conjunction of a set of clauses. A disjunctive normal form (DNF) is just a CNF where the two operators ∧ (and) and ∨ (or) are exchanged. In the following formula the first is a CNF, while the second is a DNF :

Various Boolean operators can be transformed into each other (where the symbol ⇐⇒ is used in the sense “is equivalent to”). 9 identities are listed below.

(1) It is possible to eliminate one of the three operators (negation, and, or) using the following identities (Morgan’s law):

(2) The implication and the reverse implication can be replaced using:

(3) Boolean equivalence can be substituted using:

(4) The exclusive or is also defined as follows:

(5) The operators nand and nor are given by a negation in Table 1:

(6) The indexed operators have the following meanings (where all x_{i} are Boolean propositions
and i ∈ I = {1,…,n},n > 0):

(7) The at-least operator (atleast(k)i∈I ) can also be interpreted as a CNF:

The expression on the right hand side is a conjunction of clauses consisting of exactly k positive propositions each. The at-least operator can be interpreted as a compact form of a possibly very large (containing many clauses) CNF.

(8) The four indexed operators and, or, nand, and nor can be expressed using the at-least operator using :

Interpretation: (1) If and only if all expressions are true then at least all are true; (2) if and only if one expression is true then at least one is true; (3) if not all are true then al least one is false; (4) if none is true then at least all are false.

(9) One may also replace negation of the at-least, at-most, and exactly operators by each other:

Note also that atleast(k)… with k > n and atmost(k)… with k < 0 is defined to be false. Likewise, atmost(k)… with k ≥ n and atleast(k)… with k ≤ 0 is defined to be true.

Using the substitutions (1) to (9) given above one can easy see that all logical operators can be reduced to a few once, for example, negation (¬), and (∧), or (∨), and the at-least (atleast() ) operator. The next section shows how these identities can be used to translate logical expressions into pure mathematical formulas.