The basic idea is to represent each subplan as though it was developed in a context. These contexts will differ, either slightly or greatly. The terminology within each subcontext is likely to be specialized, and making the plans work together requires some generalization. For this purpose we use lifting formulas, i.e. formulas that relate the propositions and terms in subcontexts to propositions and terms in an outer context.
Here is an example. Assume that a route planner, like the route optimization program of the TRAINS project [3], and a supply planner, like the transportation scheduler developed at Kestrel [53], have been developed independently by different groups. Given a source and a destination, the route planner will find the best route between these places. It however, has no notion of which supplies need to be transported and no notion of time. The supply planner keeps track of the supplies of some economic system and informs us which supplies need to be moved at any given time. We assume that the supply planner has no knowledge about the routes that the supplies need to travel to reach their destination.
To fill in a work order we need to integrate the information produced by the supply planner with that of the route planner. Assume that the supply planner produces
informing us that equipment1 needs to be transported
from Rome Air Force base in New York on 11/6/95, to
Frankfurt on 1/20/96. The context constant
denotes the context in which supply
planner operates and reports its results.
Now assume that the route planner tells us that
the best route from Rome to Frankfurt is via New York City
(NYC). This is represented in the context of the route planner,
, by stating
Note that is a function returning a list which encodes the best
route.
Integrating this information inside the problem solving context,
, we get
stating that equipment1 needs to be transported by the route
Rome-NYC-Frankfurt departing on 11/6/95 and arriving on 1/20/96.
This information can now be entered into the work order. Note that
the same predicate symbol, , is used in different ways in two
different contexts: its arity and its arguments are different in the
context and in the
context.
The context formalism enables us to capture this style of reasoning in logic. We write lifting axioms which describe how the information from different contexts can be integrated. In the above example the lifting formula is
If the formula is true in the context
of the supply planner, then the formula
holds in the problem solving context. Intuitively, formula 70 expresses that if the supply planner states that some items x need to be transported leaving l1 on d1 and arriving to l2 on d2, and if
is reported by the route planner as the best route from l1 to l2, then the information which can be entered into the work order is
In other
words, formula 70 specifies the integrating of a plan which
involves the notions of time and supplies produced by the supply
planner with the details involving a route produced the route planner.
The lifting axiom
70 allows us to derive the plan given by formula
69 in the problem solving context from the plans
given by formulas 67 and 68 in the contexts of their
corresponding planners.
A term with a definite meaning in one context often needs translation
when used in another context. Thus may mean Rome NY in a data
base of US Air Force bases but needs translation when a formula is
lifted to a context of worldwide geography. Lifting formulas similar
to 70 can be used to do this type of translation.