next up previous
Next: Formalization for Bargaining Up: Integrating Databases Previous: The GENavy, and

A Simple Formalization

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 tex2html_wrap_inline4168 , an ad hoc context for reasoning about the particular problem, may be required. The problem solving context tex2html_wrap_inline4172 contains objects denoting the General Electric context c_GE tex2html_wrap_inline4172 , the Navy context c_N tex2html_wrap_inline4174 , and the Air Force context c_AF tex2html_wrap_inline4176 . This enables us to talk about facts which are contained in the corresponding databases. If for example the GE database contains a fact tex2html_wrap_inline4178 then the sentence


is true in tex2html_wrap_inline4172 .

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 tex2html_wrap_inline4172 . Function tex2html_wrap_inline4186 , 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, tex2html_wrap_inline4188 is the set of spares that Navy assumes will be included in the price of the product x. Function tex2html_wrap_inline4192 , when given a product and a context, returns the name of the warranty assumed for the product in the given context. For example, tex2html_wrap_inline4194 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 tex2html_wrap_inline4198 rather than tex2html_wrap_inline4188 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 tex2html_wrap_inline4172 . Finally, the vocabulary of tex2html_wrap_inline4172 also has a function tex2html_wrap_inline4208 , which to every object assigns its corresponding price in dollars.

In the problem solving context tex2html_wrap_inline4172 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 tex2html_wrap_inline4240 :




Information about spares and warranties will not be found in the tex2html_wrap_inline4240 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 tex2html_wrap_inline4240 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 tex2html_wrap_inline4296 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.

next up previous
Next: Formalization for Bargaining Up: Integrating Databases Previous: The GENavy, and

Sasa Buvac
Sun Jul 12 14:45:30 PDT 1998