Boolean algebra

Uses Logical truth

Logical operations

NOT: ¬(𝔹) : 𝔹

AND: 𝔹 ∧ 𝔹 : 𝔹

OR: 𝔹 ∨ 𝔹 : 𝔹

XOR: 𝔹 ⊻ 𝔹 : 𝔹

Axioms

AND is commutative:
 (x:𝔹) ∧ (y:𝔹) = y ∧ x
and distributive:
 ((x:𝔹) ∧ (y:𝔹)) ∧ (z:𝔹) = x ∧ (y ∧ z)

OR is commutative:
 (x:𝔹) ∨ (y:𝔹) = y ∨ x
and distributive:
 ((x:𝔹) ∨ (y:𝔹)) ∨ (z:𝔹) = x ∨ (y ∨ z)

XOR is commutative:
 (x:𝔹) ⊻ (y:𝔹) = y ⊻ x
and distributive:
 ((x:𝔹) ⊻ (y:𝔹)) ⊻ (z:𝔹) = x ⊻ (y ⊻ z)

Simplification rules

Eliminate NOT and OR

NOT is replaced by XOR with ⊤ :
 ¬(x:𝔹) ⇒ ⊤ ⊻ x

OR is replaced by XOR and AND:
 (x:𝔹) ∨ (y:𝔹) ⇒ x ⊻ y ⊻ (x ∧ y)

Simplify AND relations

AND is ⊥ if one of its arguments is ⊥:
 (x:𝔹) ∧ ⊥ ⇒ ⊥
 ⊥ ∧ (x:𝔹) ⇒ ⊥

If one argument of AND is ⊤, the result is the other argument:
 (x:𝔹) ∧ ⊤ ⇒ x
 ⊤ ∧ (x:𝔹) ⇒ x

If the two arguments to AND are equal, the result is any of the arguments:
 (x:𝔹) ∧ x ⇒ x

Simplify XOR relations

XOR with ⊥ leaves truth values unchanged:
 (x:𝔹) ⊻ ⊥ ⇒ x
 ⊥ ⊻ (x:𝔹) ⇒ x

If the two arguments to XOR are equal, the result is ⊥
 (x:𝔹) ⊻ x ⇒ ⊥

Normalize combinations of XOR and AND:
 (x:𝔹) ∧ ((y:𝔹) ⊻ (z:𝔹)) ⇒ (x ∧ y) ⊻ (x ∧ z)