Next: Transcending Contexts Up: NOTES ON FORMALIZING CONTEXT Previous: Entering and Leaving Contexts

# Rules for Lifting

Consider a context , which expresses a static theory of the blocks world predicates and . In reasoning about the predicates themselves it is convenient not to make them depend on situations or on a time parameter. However, we need to lift the results of to outer contexts that do involve situations or times.

To describe , we may write informally

 (2)

 (3)

which stands for
 (4)

We want to apply in a context in which and have a third argument denoting a situation. In the following formulas, we put the context in which the formula is true to the left followed by a colon. denotes an outer context in which formulas not otherwise qualified are true. The next section has more about . Suppose that in context we have

 (5)

and
 (6)

thus associating a context with each situation . We also need
 (7)

which abbreviates to
 (8)

and asserts that the facts of all hold in the contexts associated with situations. Mike Genesereth points out that this necessarily involves quantifying into an . Now suppose we have the specific fact
 (9)

asserting that block is on block in a specific situation , and we want to derive . We proceed as follows.

First use () to get

 (10)

Now we enter and get
 (11)

From () and () we conclude
 (12)

from which entering gives
 (13)

() and () give
 (14)

holding in context . We can now either continue reasoning in or leave and get
 (15)

and using ()
 (16)

and finally
 (17)

In this derivation we used a function giving a context depending on the situation parameter . Contexts depending on parameters will surely present problems requiring more study.

Besides that, the careful reader of the derivation will wonder what system of logic permits the manipulations involved, especially the substitution of sentences for variables followed by the immediate use of the results of the substitution. There are various systems that can be used, e.g. quasi-quotation as used in the Lisp or KIF, use of back-quotes, or the notation of [Buvac and Mason, 1993] or the ideas of [McCarthy, 1979b], but all have disadvantages. At present we are more attached to the derivation than to any specific logical system and consider preferable a system in which the above derivation is preserved with as little change as possible.

As a further example, consider rules for lifting statements like those of section to one in which we can express statements about Justice Holmes's opinion of the Sherlock Holmes stories.

Next: Transcending Contexts Up: NOTES ON FORMALIZING CONTEXT Previous: Entering and Leaving Contexts
John McCarthy
2005-04-13