Support has been obtained for this work from the following
sources: from INRIA (first through the “Équipes
Associées” Slimmer, and the “ADT” BATT),
and from the NSF Grants CCR-0429572 (that also included
support for Slimmer) and OISE-0553462.
We avoid the usual names (logic variables for existential
variables and eigenvariables for universal variables) in order
to clearly separate the high-level description given here from the
implementation, which is not detailed here, but in which the class of
a variable isn’t static.
Actually, such names exist and are accepted by the parser, but
are rejected in type, constant and predicate declarations, as they are
read-only names, only used for undocumented, internally defined
predicates (usually experimental, non-logical, and with side-effects).