A context is a structure with three components: 1) a set of hypotheses; 2) a restriction set; 3) a set of names. The set of hypotheses is a set of nodes which are the assumptions of the context. The set of hypotheses is the determining component of the context in the sense that no two contexts will have the same set of hypotheses. The restriction set is a set of sets of nodes, such that the union of any of these sets with the set of hypotheses of the context forms a set of hypotheses from which a contradiction has been derived (i.e. a set of hypotheses known to be inconsistent). The set of names is a set of symbols each of which functions as a name of this context.
A context name intensionally defines a context , which is extensionally defined by its set of hypotheses. The SNePSUL user always refers to contexts by name , and may add assertions to, or remove assertions from a context. Actually, such changes do not change contexts (extensionally defined), but change the context that the name refers to. The system takes care of such details, and the SNePSUL user may normally think of a context name as always referring to the same context.
The user is always working in a particular context, called the current context . The current context for a particular SNePSUL command may be specified by an optional argument to the command. Otherwise, all commands are carried out with the default context as current context. By default, this context is named default-defaultct .
In SNePS 2.3 and later versions, a proposition node is not simply asserted or unasserted --it is either asserted or unasserted in each context. The ! suffix will be printed with a node's name when that node is asserted in the current context. An hypothesis is a node that was asserted by the user using assert or ! , rather than being asserted only because it was derived during inference. An hypothesis is always an hypothesis of one or more context; it may also be asserted in other contexts, and might be unasserted in still other contexts.
Every node is said to be in zero or more contexts . A node n is in a context c in any of the following cases: