In this simple case, assume that the
Air Force and Navy data bases need
to be updated on the new General Electric prices.
The GE database lists the list price, i.e.
the price at which GE is selling the engine.
The Navy database lists the price which
Navy *will need to pay* for the engine
and its assortment of spare parts, if it
decides to use GE.

In order to reason with multiple databases,
*c_ps* , an ad hoc context for reasoning
about the particular problem, may be
required.
The problem solving context
contains objects denoting the
General Electric context *c_GE* ,
the Navy context *c_N* ,
and the Air Force context *c_AF* .
This enables us to talk about facts which are
contained in the corresponding databases.
If for example the GE database contains a fact
then the sentence

is true in .

Different data bases might make different
assumptions.
For instance,
prices of engines in some contexts
might or might not include spare parts or
warranties.
We need the
ability to represent this information
in .
Function , when given a product and
a context, returns the spares which the given
context assumes necessary and thus includes in
the price of the product.
For example, is the set
of spares that Navy assumes will be included
in the price of the product *x*.
Function , when given a product and
a context, returns the name of the warranty
assumed for the product in the given context.
For example, is the
name of the warranty which Navy assumes is
included in the price of the product *x*.
In this note we are treating warranty in the
same manner as we would treat spare parts or
additional optional features.
It would be the responsibility of another
formalization to ``understand'' the warranty
and give axioms describing the exact obligations
that GE has to its clients.
Note that information about spares and
warranties assumed by
the Navy will probably not be
contained in the Navy data base.
(Otherwise, we would use
rather than to refer to
the spares that Navy assumes will be included
in the price of the product *x*.)
Rather, this information is kept in in some manual.
But for these data bases to be used jointly,
the spares information needs to be included;
we assume that it is described
declaratively in .
Finally,
the vocabulary of also has
a function , which to every object
assigns its corresponding price in dollars.

In the problem solving context we also represent the fact that GE lists engine prices without any spares, while Navy assumes spare parts to be included in the price of a product. This is done by lifting axioms, which define how the notion of price in different databases translates into the problem solving context:

expressing that the price listed in the Navy data base is the price of the engine, some bag of spares, and the particular warranty that are assumed by the Navy.

where *f* is some function which determines
the total price of an item and spares, also
taking into account the inventory cost.
Note that *f* might not be precisely known,
in which case we might decide to only give
some approximate bounds on *f*.

Now we work out an example. Assume that we are given the prices as listed in the GE data base; i.e. the following formulas hold in :

Information about spares and warranties will not be found in the data base and will probably require looking up in some manual or description of the the data base. We need to enter this information into the the problem solving context:

Then we can compute the price of the FX-22 jet engine for the Navy. The following formula is a theorem, i.e. it follows from the above axioms.

**Theorem (engine price):**

In order to compute this price for the Air
Force, the inventory cost given by
function *f* would need to be known.

**Proof !engine price(engine price):**
First we exit the context thus rewriting formulas
43, 44, and 45 as

From formulas 40 and 48 it follows that

From formulas 40 and 49 it follows that

Therefore, using formula 46, we get

In a similar fashion, from formulas 40, 47 and 50 we can conclude that

From formulas 51, 53, and 54 if follows that

Then, using formula 41 we can conclude that

By entering we get

In the above proof we are assuming that all constants denote the same
object in all contexts, i.e. that all constants are *rigid designators*.
Consequently constants can be substituted for universally quantified
variables by the universal instantiation rule.
Generalizing the proof is straight forward if we drop this assumption.

Sun Jul 12 14:45:30 PDT 1998