4.2. Constraint Propagation🔗

For all the propositions in the True and False equivalence classes, there are of course basic facts, e.g. about logical combinations of these statements, that can be derived. This is what constraint propagation does. Among others, it considers the following:

• Boolean Connectives (e.g. a conjunction is true then both conjuncts are true)

• Inductive Types (e.g. if some a = some b then a = b)

• Projections (e.g. if (a₁, a₂) = (b₁, b₂) then a₁ = a₂)