The original proposals for context, [McC87b, McC93], have influenced a number of researchers to develop logics of context; these include [Sho91, Guh91, GSGF93, Nay94, AS95, BBM95, Buv96a]. We proceed with a short description of the logical properties of contexts and contextual reasoning.

1. Contexts are treated as formal objects, i.e. objects in the semantics which
can be denoted by constants in the language and over which variables can range.
Treating contexts as formal objects allows us to state relations between
contexts in the same way we state relations between any other objects in the
logic. For example, we can define a relation *Specializes*(*c*1,*c*2) which holds
when context *c*2 is a specialization of context *c*1.

2. We introduce a new modality *ist* which is pronounced ``is true''.
Formulas of the form
are to be taken as assertions that the proposition *p* is true in context *c*.
This allows us to express that, for example, John McCarthy is a professor in the
context of Stanford University: . Note that sentences of the form *ist*(*c*,*p*) can
themselves be true in contexts, e.g. we can have *ist*(*c*1,*ist*(*c*,*p*)). The
*ist* modality also allows us to state *lifting axioms*--axioms relating
what is true in one context based on what is true in another context. Lifting
axioms are central for reasoning with multiple contexts; we will give examples
of lifting axioms throughout the following sections.

3. All formulas are stated in some context, so we write when
formula is given in context *c*. There is no outermost context; it is
always possible to *transcend* the outermost context so far referred to.
Transcendence is discussed in [McC93].

4. In order to capture the intuitive patterns of contextual reasoning, the
formal system needs to contain rules for entering and exiting a context. For
example, suppose we have the formula *c*0:*ist*(*c*,*p*). We can then *enter*
the context *c* and infer the formula *c*:*p*. Conversely, if we have the formula
*c*:*p* we can infer *c*0:*ist*(*c*,*p*) by *exiting* the context *c*.

5. Besides propositions being true in contexts, we also need the ability to
talk about a value of a term *t* in context *c*, which we will write as
*Value*(*c*,*t*). For example, we may need , when *c*
is a context that has a time, e.g. a context usable for making assertions about
a particular situation. In [MB94], we show how formulas
containing the *Value* function can be treated as abbreviations of formulas
containing *ist*.

Sat Mar 15 22:18:39 PST 1997