This class contains logical connectives, most of them derive
from this class. If you want to create a term with a connective
that is stored in this class you have to take this one, because
these operators are handled as singleton so that e.g.
these operators are compared using equality on references not on
names.
the ususal 'forall' operator 'all' (be A a formula then
'all x.A' is true if and only if for all elements d of the
universe A{x<-d} (x substitued with d) is true
the ususal 'exists' operator 'ex' (be A a formula then
'ex x.A' is true if and only if there is at least one elements
d of the universe such that A{x<-d} (x substitued with d) is true
the wary substitution operator {var<-term}'. {x<-d}'A(x) means
replace all free occurrences of variable x in A with d, however
without replacing x with a non-rigid A below modalities
the throughout operator of dynamic logic. A formula
[[alpha;]]Phi can be read as 'In all intermediate states during
processing the program alpha the formula Phi holds'.