ATOM ::= TRUTH | PREDICATION | DEFINEDNESS
| EXISTL-EQUATION | STRONG-EQUATION
An atomic formula ATOM is well-formed (with respect to the local environment and variable declarations) if it is well-sorted and expands to a unique atomic formula for constructing sentences. The notions of when an atomic formula is well-sorted, of when a term is well-sorted for a particular sort, and of the expansions of atomic formulae and terms, are indicated below for the various constructs.
Due to overloading of predicate and/or operation symbols, a well-sorted atomic formula or term may have several expansions, preventing it from being well-formed. Qualifications on operation and predicate symbols may be used to determine the intended expansion and make it well-formed; explicit sorts on arguments and/or results may also help to avoid unintended expansions.