Goals of the ATMS
The main goal of a TMS is to compute the label of each node. The ATMS guarantees that labels are:
consistent: every environment in it is consistent
sound (correct): the node is derivable from each environment of the label;
complete: every consistent environment in which the node holds is either in the label or a superset of an environment in the label;
minimal: no environment in the label is a superset of any other.
By computing labels, the ATMS is able to maintain all the possible contexts.