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.