Boolean algebra

Konrad Hinsen

Context boolean
uses builtins/truth

1 Logical operations

The following operators are defined on terms of sort boolean:

NOT:		¬(boolean) : boolean
AND:		boolean ∧ boolean : boolean
OR:		boolean ∨ boolean : boolean
XOR:		boolean ⊻ boolean : boolean

1.1 Rewrite rules

1.1.1 Eliminate NOT and OR

NOT is replaced by XOR with true:

¬(X) ⇒ true ⊻ X ∀ X : boolean

OR is replaced by XOR and AND:

X ∨ Y ⇒ X ⊻ Y ⊻ (X ∧ Y) ∀ X : boolean ∀ Y : boolean

1.1.2 Simplify AND relations

AND is false if one of its arguments is false:

X ∧ false ⇒ false ∀ X : boolean
false ∧ X ⇒ false ∀ X : boolean

If one argument of AND is true, the result is the other argument:

X ∧ true ⇒ X ∀ X : boolean
true ∧ X ⇒ X ∀ X : boolean

If the two arguments to AND are equal, they are also equal to the result:

X ∧ X ⇒ X ∀ X : boolean

1.1.3 Simplify XOR relations

XOR with false leaves truth values unchanged:

X ⊻ false ⇒ X ∀ X : boolean
false ⊻ X ⇒ X ∀ X : boolean

If the two arguments to XOR are equal, the result is false:

X ⊻ X ⇒ false ∀ X : boolean

1.1.4 Standardize combinations of XOR and AND

The above rules will reduce any boolean expression to a combination of XOR and AND operations that allow no further simplification. However, it is still possible that logically equal expressions are rewritten into distinct syntactical forms, making it difficult to verify that they are equal. The following rule standardizes results by replacing XOR inside AND by AND inside XOR:

X ∧ (Y ⊻ Z) ⇒ (X ∧ Y) ⊻ (X ∧ Z)
  ∀ Z : boolean
  ∀ X : boolean
  ∀ Y : boolean

1.2 Tests

Truth table for Not:

¬(false) ⇒ true ✓
¬(true) ⇒ false ✓

Truth table for AND:

false ∧ false ⇒ false ✓
false ∧ true ⇒ false ✓
true ∧ false ⇒ false ✓
true ∧ true ⇒ true ✓

Truth table for OR:

false ∨ false ⇒ false ✓
false ∨ true ⇒ true ✓
true ∨ false ⇒ true ✓
true ∨ true ⇒ true ✓

Truth table for XOR:

false ⊻ false ⇒ false ✓
false ⊻ true ⇒ true ✓
true ⊻ false ⇒ true ✓
true ⊻ true ⇒ false ✓