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.
