John McCarthy <jmc@sail.stanford.edu>
Reply-To: cg@cs.umn.edu
Date: Tue, 29 Sep 92 20:47:13 -0700
From: John McCarthy <jmc@sail.stanford.edu>
Message-id: <9209300347.AA23509@SAIL.Stanford.EDU>
To: sowa@watson.ibm.com
Cc: SRKB@isi.edu, INTERLINGUA@isi.edu, CG@cs.umn.edu, buvac@cs.stanford.edu,
costello@cs.stanford.edu, guha@mcc.com
In-reply-to: sowa@watson.ibm.com's message of Tue, 29 Sep 92 22:03:11 EDT <199209300208.AA01752@venera.isi.edu>

The contexts that Guha and Sasa Buvac and I have studied are a lot
more ambitious than any of the three possibilities you list, and
I think this greater ambition is appropriate to Intelingua/KIF.

1. A packaging mechanism for enclosing a collection of formulas and
allowing them to be named and referenced as a single unit.

2. The contents of that package, which could be called anything from
"quoted formula" to "microtheory".

3. The permissible operations on the formulas in the package.  These
operations could be defined by a set of axioms in a larger package
that encloses the one under discussion.

You choose the packaging mechanism alternative and give the
following examples.

1. "The conjunction of the formulas in this box is false."

2. "The formulas in this box describe a possible state of affairs."

3. "Mary believes the propositions stated by the formulas in this box."

4. "The formulas in this box interact according to the axioms contained
in the box named S5."

5. "The formulas in this box were true during the time interval [t1,t2]."

6. "Any formula placed in this box must be in Horn-clause form."

None of the six examples relate formulas in the box to formulas
outside the box.  Our work is entirely based on {\it lifting formulas}
that relate a formula in an inner context to formulas outside
the box.

Examples:

A certain context  c1  may refer to a fixed time interval.  In that
context a formula

at(McCarthy, residence(McCarthy))

may be true.  To lift this formula out of the context into a more
general context  c2  in which the referent of "McCarthy" is defined but
a specific evening is not, we use a lifting relation

ist(c1,p) iff ist(c2, holds(1992 Sept 29 8pm-9pm,p)).

To lift the formula to a more general context  c3  in which "McCarthy"
hasn't a definite referent, it is necessary to use another lifing
relation.

I think even the simplest applications to databases require formulas
that change on lifting.  To take an example from our recent proposal,
the Airforce, the Navy, and General Electric Company may all have
databases of airplane engines and their prices, but they may differ
in assumptions about spare parts.  Using the databases together
requires a more general context to which the formulas from the
specialized databases can be lifted but translated appropriately.

I'm sure that communication among programs will also require lifting
relations.