  Proposition algebra is based on Hoare's conditional connective, which is a
ternary connective comparable to if-then-else and used in the setting of
propositional logic. Conditional statements are provided with a simple
semantics that is based on evaluation trees and that characterizes so-called
free valuation congruence: two conditional statements are free valuation
congruent if, and only if, they have equal evaluation trees. Free valuation
congruence is axiomatized by the four basic equational axioms of proposition
algebra that define the conditional connective. Valuation congruences that
identify more conditional statements than free valuation congruence are
repetition-proof, contractive, memorizing, and static valuation congruence.
Each of these valuation congruences is characterized using a transformation on
evaluation trees: two conditional statements are C-valuation congruent if, and
only if, their C-transformed evaluation trees are equal. These transformations
are simple and natural, and only for static valuation congruence a slightly
more complex transformation is used. Also, each of these valuation congruences
is axiomatized in proposition algebra. A spin-off of our approach can be called
"normalization functions for proposition algebra": for each valuation
congruence C considered, two conditional statements are C-valuation congruent
if, and only if, the C-normalization function returns equal images.
