From: AAAI-93 Proceedings. Copyright © 1993, AAAI ([Link]). All rights reserved.

Propositional Logic of Context

Saga BuvaE & Ian A. Mason
Computer Science Department
Stanford University
Stanford
California 94305-2140
{buvac, iam}@[Link]

Abstract Furthermore, it seems that the context formalism can

provide semantics for the process of translating facts
In this paper we investigate the simple logical into KIF and from KIF, one of the key tasks that the
properties of contexts. We describe both the syn- knowledge sharing effort is facing.
tax and semantics of a general propositional lan-
The meaning of an utterance depends on the context
guage of context, and give a Hilbert style proof
in which it is uttered. Computational linguists have
system for this language. A propositional logic
developed various ways of describing this context. For
of context extends classical propositional logic in
example, Barbara Grosz in her Ph.D. thesis, [Grosz,
two ways. Firstly, a new modality, ist(K, 4), is in-
19771, implicitly captures the context of a discourse
troduced. It is used to express that the sentence,
by focusing on the objects and actions which are most
4, holds in the context 6. Secondly, each context
relevant to the discourse. This representation is similar
has its own vocabulary, i.e. a set of propositional
to an ATMS context [de Kleer, 19861, which is simply
atoms which are defined or meaningful in that con-
a list of propositions that are assumed by the reasoning
text. The main results of this paper are the sound-
system.
ness and completeness of this Hilbert style proof
system. We also provide soundness and complete- However till now no formal logical explication of con-
ness results (i.e. correspondence theory) for vari- texts has been given. The aim of this paper is to rectify
ous extensions of the general system. this deficiency. We describe both the syntax and se-
mantics of a general propositional language of context,
and give a Hilbert style proof system for this language.
Introduction The main results of this paper are the soundness and
In this paper we investigate the simple logical proper- completeness of this Hilbert style proof system. We
ties of contexts. Contexts were first introduced into AI also provide soundness and completeness results (i.e.
by John McCarthy in his Turing Award Lecture, [Mc- correspondence theory) for various extensions of the
Carthy, 19871, as an approach which might lead to the general system.
solution of the problem of generality in AI. This prob-
lem is simply that existing AI systems lack generality. Notation
Since then, contexts have found a large number of
uses in various areas of AI. R. V. Guha’s doctoral dis- We use standard mathematical notation. If X and Y
sertation [Guha, 19911 under McCarthy’s supervision are sets, then X +, Y is the set of partial functions
was the first in-depth study of context. Guha’s con- from X to Y. I?(X) is the set of subsets of X. X* is the
text research was primarily motivated by the Cyc sys- set of all finite sequences, and we let 3 = [xi, . . . , ~~1
tem [Guha and Lenat, 19901 (a large common-sense range over X*. 6 is the empty sequence. We use the
knowledge-base currently being developed at MCC) . infix operator * for appending sequences. We make
Without using contexts it would have been virtually no distinction between an element and the singleton
impossible to create and successfully use a knowledge sequence containing that element. Thus we write z *ICI
base of the size of Cyc. instead of z * [ICI]. As is usual in logic we treat X*
Large knowledge bases are not the only place where as a tree (that grows downward). ~1 < ~0 2 E iff ~1
contexts have found practical use. The knowledge properly extends 30 (i.e. (3~ E X* - {E})(z~ = ZO*$).
sharing community has accepted the need for expli- We say Y C X* is a subtree rooted at g to mean
cating context when transferring information from one
agent to another. Currently, proposals for introduc- 1. $i E Y and (VZ E Y)(z 5 y)
ing contexts into the Knowledge Interchange Format or
KIF [Genesereth and Fikes, 19921 are being considered. 2. (Vz E Y)(Vw E X”)(x 5 a 5 Q + ti E Y)

412 Buvac
 The General System restrictions on what kinds of structures are allowed as
models, as well as enriching the axiom system.
A propositional logic of context extends classical
Secondly, a context is modelled by a set of truth as-
propositional logic in two ways. Firstly, a new modal-
signments, that describe the possible states of affairs of
ity, ist(K, 4), is introduced. It is used to express that
that context. Therefore the ist modality is interpreted
the sentence, 4, holds in the context K. Secondly, each
as validity: ist(K, p) is true iff the propositional atom
context has its own vocabulary, i.e. a set of proposi-
p is true in all the truth assignments associated with
tional atoms which are defined or meaningful in that
context tc. Treatment of ist as validity corresponds to
context. The vocabulary of one context may or may
Guha’s proposal for context semantics, which was mo-
not overlap with another context.
tivated by the Cyc knowledge base. A system which
Syntax models a context by a single truth assignment, thus
interprets ist as truth, can be obtained by placing
We begin with two distinct countably infinite sets, R simple restrictions on the definition of a model, and
the set of all contexts, and EOthe set of propositional enriching the set of axioms.
atoms. The set, w, of well-formed formulas (wffs) is Thirdly, since different contexts can have different
built up from the propositional atoms, p, using the vocabularies, some propositions can be meaningless in
usual propositional connectives (negation and implica- some contexts, and therefore the truth assignments de-
tion) together with the ist modality. scribing the state of affairs in that context need to be
partial.
Definition (W):
Definition (9X): In this system a model, ??X, will
be a function which maps a context sequence E E lK*
The operations A, V and ++ are defined as abbrevia- to a set of partial truth assignments,
tions in the usual way. The term literal is used to refer
to a propositional atom or the negation of a proposi- .!I2E lEc*--+P P(P +-P 2),
tional atom. We use 4$ to represent either the formula
with the added conditions that
4, or its negation 14. We also use the following abbre-
viations: 1. (VE)(V’vi, z4 E !B@))(Dom(vi) = Dom(v2))
ist(X,qS) := ist(bcl,ist(m,...,ist(h,+))) 2. Dam(m) is a subtree of K* rooted at some context
sequence Kc.
ist*(iZ,+) := fist(6~,fist(z.2,-..
kiiSt(fin,q5)-.-))
We write EM to denote the set of partial truth as-
when E is the context sequence [IE~,~2, . . . , ~~1. In the signments 9X(E). Note that Em can be empty. The
definition of ist * all the ist’s need not be of the same collection of all such models will be denoted by Ml.
parity. PROP is the set of all well formed formulas We could have assumed the existence of a fixed out-
which do not contain ist’s. If $Jis a formula containing ermost context which would result in Dom(fm) being
distinct atoms pi,. . . ,pn, then we write $J(&, . . . , &) a tree rooted at empty sequence E (i.e. the fixed out-
for the formula which results from $Jby simultaneously ermost context). This would result in slightly simpler
replacing all the occurrences of pi in $ by 4;. We say notation and proofs. However, although more com-
that $+A,. . . , Ad is an instance of $. plicated, our definition is based on the intuition that
there is no outermost context.
Semant its
Vocabularies The truth assignments in our model
We begin with a system which makes as few semantic
are partial. The atoms which are given a truth value
restrictions as possible. Other systems are obtained by
in a context are defined by a relation Vocab E lK* x IED.
placing restrictions on the models. The semantics of
the general system has the following three features:
Firstly, the nature of a particular context may itself Definition (Vocub of tm): We define a function
be context dependent. For example, in the context of Vocub : Ml + P(IK* x p) which given a model returns
the 1950’s, the context of car racing is different than the vocabulary of the model:
than the context of car racing viewed from today’s con- Vocub(9X) := {<E, p> ] E E Dom(9X) and p E Dom(!?Q))}
text. This leads naturally to considering sequences of
contexts rather than a solitary context. We refer to this We say that a model iDIis cZussicuZon vocabulary Vocab
feature of the system as non-flatness. It reflects on the iff Vocab C Vocub(?DQ.
intuition that what holds in a context can depend on The notion of vocabulary can also be applied to sen-
how this context has been reached, i.e. from which per- tences. Intuitively, the vocabulary of a sentence relates
spective it is being viewed. For example, non-flatness a context sequence to the atoms which occur in the
will be desirable if we represent the beliefs of an agent scope of that context sequence. In the definition we
as the sentences which hold in a context. A system of also need to take into account that sentences are not
flat contexts can easily be obtained by placing certain given in isolation but in a context.

NonmonotonicLogic 413
Definition (Vocab of 4 in E): We define a function Assuming that our system was limited to only one
Vocab : K* x !4’ + P(K* x P) which given formula context, the rule (CS) would be identical to the rule
in a context, returns the vocabulary of the formula. of necessitation in normal systems of modal logic, and
Vocab(E, 4) is defined inductively by: axiom schema (IX) would be identical to the the stan-
dard axiom schema K. Thus in the single context case,
ignoring axiom schemas (A+) and (A-), our formal
system is identical to what is usually called the normal
system of modal logic, characterized by (PL), (NIP),
(K), and the rule of necessitation. The axiom schemas
(A+) and (A-) are needed in order to accommodate
It is extended to sets of formulas in the obvious way. the validity aspect of the ist modality. It turns that
Note that it is only in the propositional case that they derivable in the system which treats ist as truth
we can carry out this static analysis of the vocabulary and does not allow inconsistent contexts.
of a sentence. It will not be possible in the quantified
Provability A formula q5 is provable in context K
versions. Also note that our definition of vocabulary of
with vocabulary Voca b (formally l-z 4) iff I-, 4 is an in-
a sentence is somewhat different from Guha’s notion of
stance of an axiom schema or follows from provable for-
definedness. Guha proposes to treat ist(K, 4) as false
mulas by one of the inference rules; formally, iff there
if 4 is not in the vocabulary of the context K.
is a sequence [ l-x1 41, . . . , l-z, &] such that En = E,
Satisfaction We can think of partial truth assign- and A = 4 and for each i 5 n either l--z%+i is an
ments as total truth assignments in a three-valued axiom, or is derivable from the earlier elements of the
logic. Our satisfaction relation then corresponds to sequence via one of the inference rules. In the case
Bochvar’s three valued logic [Bochvar, 19721, since an of assumptions, formula 4 is provable from assump-
implication is meaningless if either the antecedent or tions T in context Ee with vocabulary Vocab (formally
the consequent are meaningless. We chose Bochvar’s T ,Joca b or again taking into account that Vocab is
three valued logic because we intend meaningfulness to fixed T &, 4) iff there are formulas 41,. . . ,& E T,
be interpreted as syntactic meaningfulness, rather than such that l-z0 (41 A . . . A &) --+ 4. Note that due to
semantic meaningfulness along the lines of Kleene’s the definedness convention if T l-z, 4 then Vocab(T) E
three valued logic [Kleene, 19521. Voca b.

Definition (b) : Consequences

If v E Ed and Vocab(E,cp) G Vocub(iDl), then Some simple theorems and derivable rules of the sys-
9JZ,vk,piffv(p)=l, pEP tern are:
!X$~~~+iffnot%R,v&+ (C) I--, ist(Ki,$) A ist(Ki,ti,) -+ ist(Ki,+A+)
~,v~,~~~iff~,y~~~implies~,v~,Ijl (Or) I-.C ist(Ki,+) V ist(Ki,1CI) --+ ist(Ki,+V+)
9X, u k, ist(Ki, 4) iff Vvl E (E*KI)~ 9X, VI j=z*Kl 4 (M) t-, ist(m, 4 A $1 --+ ist(Ki, 4) A ist(ni, $J)
In the last point note that i? * ~1 E Dom(9.X) since (K*) l-c ist(z, 4 -+ $J) + ist(c, 4) --+ is@‘, $>
the Dom(!.?X) is a rooted subtree, and Vocab(E, 4) C
Vocub(m).
Wewritet)171+,4iffVvEiP ?JX,Ykf+.

Formal System
We now present the formal system. To do this we fix
a particular vocabulary, Vocab c K* x P, and define A slightly deeper result is that any formula is prov-
ably equivalent to one in a certain syntactic form. This
a provability relation, t-G
‘Ocab. Since Vocab will re- equivalence plays an important role in the complete-
main fixed throughout we omit explicitly mentioning it ness proof.
and write l-,4 instead. Similarly, to avoid constantly
stating lengthy side conditions we make the following Definition (CNF) : A formula 4 is in conjunctive
convention. normal form (CNF) iff it is of the form Ei A E2 A - - . A
EI,, and each Ei is of the form oil V ai V - - - V aiTz,
Definedness Convention: In the sequel, when- where each oij is either a literal, or ist*(i?, ,0) for some
ever we write l--,4 we will be assuming implicitly that disjunction of literals ,0. Note that i and k can be 1.
Vocab(E, 4) C Vocab.
Axioms and inference rules are given in table 1. Note Lemma (CNF): For any formula 4, context se-
that the rules of inference preserve the (definedness quence E, there exists a formula $* which is in CNF,
convention). such that l-z+ H +*.

414 Buvac
 :(PL) )-F 4 provided 4 is an instance ofa tautology.

(K) t-, ist(m, 4 -+ @> +ist(1~1,q5)-+ist(Kl,$)

(A,) t--s;r
ist(/cl,ist(Kz,qS)V+)+ist(m,ist(K2,4))V ist(m,$,)
(A-.) I-, ist(Kl,list(K2,~$) --+ist(Ki,
V 7j3) ++2,+>> V ist(Ki, $)

h& ~id--+ti hT*/q 4

WY w
bb t-z isth, 4)

Table 1: Axioms and Inference Rules

Theorem (soundness) : If I-F~, then for all mod- extend T to a maximally consistent set To. From To we
els f)32classical on Vocab ?JXk=s;r4. If T I-F 4, then for will construct the model 9X0. For each i? = Ec * C E JK*
all models 9.X classical Vocab if for all 1c,E T 9X j=~ define
$J, then 9X +E 4.
Tic+ := (4 ITo ho ist(?, $), 4 E PROP}.
Completeness
We begin by introducing some concepts needed to state Lemma (T,+): T,+ is closed under logical con-
the completeness theorem. sequence: for all 4 where Vocab(i?, 4) & Vocab, if 4
tautologically follows from T,+ then 4 E T,+.
Definition (satisfiability): A set of formulas T is
satisfiable in context E with vocabulary Vocab iff there
Note that T,+ need not be either maximally consistent
exists a model !JX classical on Vocab, such that for all
or even consistent. Now, using only the sets T,+ of
4 E T, i-m +F 4. formulas from PROP, we will define a model ?JXc for
A formula q5is consis- the set of formulas To. We define the domain of 9X0
Definition (consistency):
tent in ET with Vocab, where Vocab@, 4) C Vocab iff Dom(!JXc) := {El E 5 ito, 32 E Dom(Vocab), TC’5 I?}
not l-x 14. A finite set T is consistent in 7Fwith Vocab
iff /x\ T is consistent in E with Vocab. An infinite set T and for all i? E Dom(!JJZc)
is consistent in in with Vocab iff every finite subset of T i%&(Z) := {v 1Dam(v) = Vocab@), E Tn+,v($)
VC#I = 1).
is consistent in i? with Vocab. A set T is inconsistent
in E with Vocab iff the set T is not consistent in 7Zwith In the above, V is the unique homomorphic extension
Voca b. of v with respect to the propositional connectives. To
A set T is maximally consistent in E with Vocab iff see that 9X0 as defined is a model, we first note that
T is consistent in E with Vocab and for all 4 $ T such it clearly meets condition 1, since all the truth assign-
that Vocab(& 4) 2 Vocab, T U {4} is inconsistent in E ments associated with a context must have the same
with Vocab. domain. Condition 2 is met since Dom(9Xo) as defined ,
As is usual, an important part of the completeness is a subtree rooted at 7~0. Note that if T,+ is empty
proof is the Lindenbaum lemma allowing any consis- (which corresponds to the case where Vocab(K) = S),
tent set of wffs to be extended to a maximally consis- then 9&(E) is a singleton set, whose only member is
tent set. the empty truth assignment. Finally, to establish com-
pleteness we need only prove the truth lemma. The
Lemma (Lindenbaum) : If T is consistent in E proof of the truth lemma is based on the CNF con-
with Vocab, then T can be extended to a maximally struction and is the novel aspect of this completeness
consistent set To in E with Vocab. proof.
Now we proceed to state and prove the completeness
of the system. Lemma (truth):
For any 4 such that Vocab(Ec, 4) E Vocab,
Theorem (completeness) : For any set of formulas
T, T is consistent in Kc with Vocab iff T is satisfiable 4 E To 8 m0 bzo 4.
in i?e with Vocab.

Proof (completeness) : Assume T is consistent in Clearly, if 4 E T then also 4 E To and therefore by

Kc with Vocab. By the (Lindenbaum lemma) we can tr uth
lemma
we
gemot
b z,
6qcompleteness
Nonmonotonic Logic 415
Before we give the proof of the truth lemma, we need axiom schema (D) w.r.t. the set of consistent models,
to state a property of the model 9X0 which is needed dealt with shortly. Formula (D,) is equivalent to
in the ist case of the truth lemma.

Lemma (930): Let 9.X0be a model as defined from for all 4 satisfying the definedness condition; the proof
To in the completeness proof. Then for all 4 E PROP carries over from normal systems of modal logic. Now
where Vocab(zo * Z, 4) s Vocab, we state a useful consequence of (D,) ‘s.

To l--z0ist@, 4) iff for all v E 9JZc(Es*C) ~(4) = 1. Lemma (Dc):

Let c be ~1 * -. a* [Link] D(,,,...,,n-,~ E To, then
ist*(?, 4) E To iff f ist@, 4) E To
A frequently used instance of the .9X0 lemma is that
To t-+, ist(?, 4 A +) iff fme(Ee * i?) = 0, for all 4 sat- for any formula 4 which satisfies the definedness con-
isfying the (definedness condition). vention. The sign on the right hand side is positive iff
there is an even number of negations in the ist* on
Proof (truth lemma): Instead of proving 4 E To the left hand side.
iff ?3XeFE0 4 we will prove the statement Now we examine the two cases need to prove the
inductive step for ist of the truth lemma.
(TL) $ is in CNF implies (+!JE To iff 9,7&o
+Fo $) .
Case D(,l,...,,,-l) E TO: In this case we assume
To see that the former follows from the latter, assume
D( K,l*“‘
*Kn-l) E To and that $ E To. Then by the D,
q5E To. By the (CNF lemma), there exists formula
lemma:
$* in CNF such that I-,, 4 H 4*. Using maximal
consistency of To, it follows that +* E To. Therefore ist*(iZ, x) E To iff f ist(?, x) E To
by (TL) it must be the case that 9X0 I=,, 4*. Our We only include the positive case.
logic is sound: 930 FE0 4* iff 9X0 bn, 4, and thus
ist@, x) E To iff To l--z, ist(?, x)
we conclude that ?JXc bTzb 4. We can simply reverse
the steps of the argument to prove the other direction Now by (?%VO lemma) and the definedness condition
of the biconditional. Vocab@e * i?) 5 Vocab we have
We prove the (TL) by induction on the structure of To l-z,, ist(7, x) iff (Vv E ?3Xo(i?))(i7(~) = 1)
the formula $J. In the base case $Jis an atom, and thus
in CNF. Prom the definition of ?JXo(Ee) it follows that By the definition of satisfaction:
p E To H 9X0 kc, p. In proving the inductive step we (Vv E Dl0(72))(Y(x) = 1) iff 1)320FE0 ist(iZ,)o
first examine $J = x V [Link] inductive hypothesis is
Now since D(,,,,,,-l) E To, and by (9Ji?olemma)
that the lemma is true for formulas x and ,x. Assume
we obtain:
x V 1-1is in CNF. Then both x and p must also be in
CNF. Since To is maximally consistent x V p E To iff ?YJZo
FE0 ist(i?,x) iff 9X0 bzo ist*(i?,)o
either x E To or p E To. By the inductive hypothesis
this will be true iff either ?3XsbEo x or 9.X0FE0 p, and
by the definition of satisfaction iff 9X0 I=,, x V p. The Case D(,l,e,,-l) @ TO: Let j be the index of the
inductive step for conjunction and negation is similar. first inconsistent context; formally D(,,,....++ $ To
We make use of the fact that if x A p is in CNF, then and D( nl*...*Kj-l) E To. Then for all 4 satisfying the
so are both x and ~1; and if lx is in CNF, then so is definedness condition we have list (Ki * . . . * ~j, q5A
x. The interesting case is when $J is an ist. Assume 14) +ZTo. Now by maximal consistency of To, (K*)
that $J is in CNF. Then II, must be of the form and (MP)
$ = ist*(i?,x), ist(Ki *. . **Kj, +AT~) E To iff ist(ni*. *.*Kj, $) E To

where x is a disjunction of literals. The context se- Thus, T(zowcl*...wcj)+ is inconsistent, 9720(Ee * ~1 * . a. *
quence c will sometimes be written as pi*. . . * K~. We Kj) = 0, and consequently
will examine two cases, depending on whether or not ist(&i *. . .*Kj, 4) E To iff ?7Xobxo ist(Ki*.. .*Kj, 4)
any of the sets of sentences T(E~*~‘)+ where C 5 2, are
for all 4 such that Vocab(Es * KI* * - - * Kj, 4) E Vocab.
inconsistent. The sets T(E,,*Ft)+, where i3 < 2, are all
Then by reasoning similar to the previous case we get:
consistent iff the formula
ist*(?,;y) E To iff ?3Xabzo ist*(?, x).
(D,) ist(Z, 14) + list@, 4)
Note that in the entire proof of the inductive step for
is in To, for any wff 4 which satisfies the definedness ist, we did not need the inductive hypothesis, making
condition. The proof of this is identical to the sound- use only of the special form of x which is guaranteed
ness and completeness proofs of a context system with because $J is in CNF. qruth-Iemma

416 Buvac
 Correspondence Results (VE E JRJ{E))(VVI, v2 E SI(E))(Dom(v~) = Dom(v2))
In this section we provide soundness and completeness The following flatness axiom schemas are sound with
results for several extensions of the general system. respect to the class of flat models Slat:
correspond to certain intuitive principles concerning
the nature of contexts. In each extension the syntax
and semantics is the same as in the general case, and (Fl+) t-z ist(K2, ist(Ki, 4)) f) is+% 4)
the (definedness convention) still holds. Only the (FL) l-z ist(K2, list(&i, 4)) --+ +st(Ki, 4)
class of models and axioms are modified.

Consistency
providing the vocabulary also satisfies the flatness con-
Sometimes it is desirable to ensure that all contexts dition: for any context sequences Tt;iand X2, and any
are consistent. context K,
In this system we examine the class, Gnsistent, of
consistent models. A model 9X E CZonsistentiff for any Vocab(El * K) = Vocab(& * K).
context sequence E E Dom(!JJX),
The backward direction of the flatness axiom
!m(iz) # 0. schemas (Fl+) corresponds of the modal logic axiom
The following axiom schema is sound with respect schema S4 (provided that ~1 is the same as ~2). Sim-
to the class of consistent models Gnsbtent: ilarly, the converse of (FL) corresponds to the modal
logic axiom schema S5. Note that the converse of (FL)
is a theorem in the system.
(D) l-z ist(E, 14) + +.st(K, 4)
It is interesting to observe that in every system with
Axiom schema (D) is also commonly used in modal ($‘I+) and (FL), (H)) is also derivable. In semantic
logic, and is sound and complete for the set of serial terms, this means that any flat model is also a con-
Kripke frames, in which for each world there is another sistent model; a reasonable property for if a context
world from which it is accessible from. Note that axiom was inconsistent, then in that context it would be true
(D) is equivalent to that all other contexts are also inconsistent. Due to
i--z ist(K, 4 A 14). flatness, this would really make all the other contexts
inconsistent.

Theorem (completeness): The general context

Theorem (completeness) : The general context
system with (D) axiom schema is complete with re-
system with (Fl+) and (FL) axiom schemas is com-
spect to the set of models Eons&tent. plete with respect to the set of flat models Slat.
Flatness
Truth
For some applications all contexts will be identical
It might be more intuitive to define the ist modality
regardless of where they are examined from. This
to correspond to truth rather than validity; incidently
type of situation will often arise when we use a num-
this is also where the ist predicate got its name: is
ber of independent databases. For example, if I am
true. Truth based interpretation of the basic context
booked on flight 921 in the context of the Northwest
modality also corresponds to the original suggestions
airlines database, then regardless of which travel agent
by McCarthy [McCarthy, 19931. In this case a context
I choose, in the context of that travel agent, it is true
is associated with a single truth assignment rather than
that in the context of Northwest airlines I am booked
a set of truth assignments.
on flight 921.
We examine the class, Truth, of truth models. A
In this system we examine a class, 5Iat, of what we
model 9X is a truth model, formally 9JiYE Zruth iff for
call flat models. A model %Ris flat, formally 9X E Slat
any context sequence E E Dam(m),
iff Dom(im) = K* and for any context sequences ~1
and &, and any context K,
rn(izl * 6) = rn(ic2 * 6). The following axiom schema is sound with respect
When dealing with flat models it might be more in- to the class of truth models Zrutlj:
tuitive to think of individual contexts rather then con-
text sequences. Then 311 E Slat can be viewed as a (Tr) I--F ist(K, 4) V ist(K, +)
function which maps contexts to finite sets of partial
truth assignments, in other words Note that (Tkr) is the converse of (D) .

?m E Ku {e} I+ P(IP dp 2). Theorem (completeness): The general context

with the side condition of general models that still ap- system with (Tr) axiom schema is complete with re-
plies: spect to the set of truth models Truth.

Nonmonotonic Logic 417

 Previously we said that (A+) and (A-) are derivable There has been other research done in this area, most
in a system which contains (D) and (Tr) . In fact, a notable is the work of Lifschitz, Shoham, and Guha.
stronger formula is true of this system: We briefly treat each in turn.
Two contexts can differ in, at least, three ways: they
l-z ist(K, # V $) f) (ist(K, 4) V ist(6, $)).
may have different vocabularies; or they may have the
same vocabulary but describe different states of affairs,
Meaninglessness as Falsity or (in the first order case) they may have the same vo-
In this section we examine a slightly more elaborate cabulary (i.e. language) but treat it differently (i.e the
modification of the general system. This modifica- arities may not be the same). The first two differences
tion closely models the semantics described, but not were studied in [BuvaE, 19921, and led to two differ-
investigated, in [Guha, 19911. The general idea here is ent views on the use of context. Lifschitz’s early note
that if 4 is not in the vocabulary of K, then ist(K, 4) on formalizing context [Lifschitz, 19861 concentrates on
is taken to be false instead of meaningless or unde- the third difference. Shoham, in his work on contexts,
fined. To cater faithfully to this interpretation, two concentrates on the second difference [Shoham, 19911.
changes must be made to the semantics of the gen- Every proposition is meaningful in every context, but
eral system. Firstly, the ist clause in the definition of the same proposition can have different truth values
Vocab : lK* x W -+ P(K* x p) must be altered to reflect in different contexts. Shoham approached the task of
the fact that ist(lc,4) will always be in the vocabu- formalizing context from the perspective of modal and
lary of any context. Secondly, the ist clause in the non-classical of logics. He defines a propositional lan-
definition of satisfaction must also be modified. The guage with an analogue to the ist modality, and a
appropriate new clause in the definition of Vocab is: relation ~1 e > ~2, expressing that context ~1 is as
general as context ~2. Drawing on the intuitive anal-
Vocab@, 4) = 0 if 4 is ist(K, $0) ogy between a context K and the proposition current-
While the new clause in the definition of satisfaction context(K), Shoham identifies the set of contexts with
is: the set of propositions. This enables him to define
truth in a context ist(K,p), in terms of the the condi-
9X, u b, ist(Ki, 4) iff Vocab(+, ?? * ~1) E Vocab(l)n) tional current-context(K) -+ p, where + is interpreted
and for all vi E (i? * ~1)~ 9X, ~1 kZeK1 4 as as some form of intuitionistic or relevance implica-
The other clauses in both definitions remain the same, tion. His paper gives a list of 14 benchmark sentences
modulo the fact that all occurrences of Vocab in the which characterize this implication.
definition of satisfaction now refer to the new defini- Guha’s dissertation contains a number of examples
tion. We maintain the (definedness convention) in of context use. These demonstrate how reasoning with
stating the proof system for this version, but again we contexts should behave, and which properties a formal-
point out that all occurrences of Vocab now refers to ization of context should exhibit. The Cyc knowledge
the new definition. The proof system for this version base [Guha and Lenat, 19901, which is the main moti-
consists of the axioms and rules of the general system, vation for Guha’s context research, is made up of many
together with the new axiom: theories, called micro-theories, describing different as-
pects of the world. Guha has tailored the design of
(MF) t-z +st(Ki,+) if Vocab(K * t~l,$) g Vocab micro-theories after contexts.
There is also a clear parallel between the logic of
context and the modal logics of knowledge and be-
The completeness proof for this system is struc-
turally similar to the one described in this paper. The lief [Halpern and Moses, 19921. The modality ist(K, 4)
only new points are those that arise out of the liberal may be interpreted as expressing that the agent K
definition of Vocab. knows or believes the sentence 4. In the case where
there is only one context, our formal system collapses
to a normal system of modal logic (with two additional
elated Work axiom schemas (A+) and (A-)). This is analogous to
Our work is largely based on McCarthy’s ideas on the way logics of knowledge and belief collapse to a
context. McCarthy’s research [McCarthy, 1987; Mc- normal system of modal logic in case of a single agent.
Carthy, 19931 in formalizing common sense has led him However, the logics of knowledge and belief differ from
to believe that in order to achieve human-like gener- our logic of contexts in a number of ways: Firstly, log-
ality in reasoning, we need to develop a formal theory its of knowledge and belief do not deal with variable
of context. The key idea in McCarthy’s proposal was vocabularies and the corresponding partiality. Fur-
to to treat contexts as formal objects, which enables thermore, logics of knowledge and belief are usually
one to state that a proposition is true in a context: ascribed possible world semantics. Consequently, an
ist(n, 4) where 4 is a proposition and K is a context. agent’s belief is modeled by relations between worlds.
This permits axiomatizations in a limited context to be Modeling truth or validity in a context by a relation be-
expanded so as to transcend their original limitations. tween worlds would not be intuitive because we want

418 Buvac
contexts to be reified as first class objects in the se- Grosz, Barbara J. 1977. A representation and use of
mantics. This will allow us (in the predicate case) to focus in a system for understanding dialogs. In Pro-
state relations between contexts, define operations on ceedings of the Fifth International Joint Conference
contexts, and specify how sentences from one context on Artificial Intelligence. Morgan Kaufmann Publish-
can be Zifted into another context. ers Inc.
Guha, Ramanathan V. and Lenat, Douglas B. 1990.
Conclusions and Future Work Cyc: A midterm report. AI Magazine 11(3):32-59.
Our goal is to extend the system to a full quantifica- Guha, Ramanathan V. 1991. Contexts: A Formal-
tion logic. One advantage of quantificational system is ization and Some Applications. Ph.D. Dissertation,
that it enables us to express relations between context, Stanford University. Also published as technical re-
operations on contexts, and state lifting rules which port STAN-CS-91-1399-Thesis.
describe how a fact from one context can be used in Halpern, Joseph Y. and Moses, Yoram 1992. A guide
another context. However, in the presence of context to completeness and complexity for modal logics of
variables it might not be possible to define the vocab- knowledge and belief. Artificial Intelligence 54:319-
ulary of a sentence without knowing which object a 379.
variable is bound to. Therefore the first step in this Kleene, Steven C. 1952. Introduction to Metamathe-
direction is to to examine propositional systems with matics. North-Holland Publishing Company.
dynamic definitions of meaningfulness.
We also plan to define non-Hilbert style formal sys- Lifschitz, Vladimir 1986. On formalizing contexts.
Unpublished manuscript.
tems for context. Probably the most relevant is a natu-
ral deduction system, which would be in line with Mc- McCarthy, John 1987. Generality in artificial intelli-
Carthy’s original proposal of treating contextual rea- gence. Comm. of ACM 30(12):1030-1035. Reprinted
soning as a strong version of natural deduction. In such in [McCarthy, 19901.
a system, entering a context would correspond to mak- McCarthy, John 1990. Formalizing Common Sense:
ing an assumption in natural deduction, while exiting Papers by John McCarthy. Ablex Publishing Corpo-
a context corresponds to discharging an assumption. ration, 355 Chesnut Street, Norwood, NJ 07648.
Finally, it would be interesting to show some for- McCarthy, John 1993. Notes on formalizing context.
mal properties of our logic. These include defining a In Proceedings of the Thirteenth International Joint
decision procedure, in the style of [Mints, 19921. Conference on Artificial Intelligence. To appear.
Mints, Grigorii E. 1992. Lewis’ systems and system
Acknowledgements
T (1965-1973). In Selected Papers in Proof Theory.
The authors would like to thank Tom Costello, R. V. Bibliopolis and North-Holland.
Guha, Furio Honsell, John McCarthy, Grigorii Mints Shoham, Yoav 1991. Varieties of context. In Lif-
and Carolyn Talcott for their valuable comments. This schitz, Vladimir, editor 1991, Artificial Intelligence
research is supported in part by the Advanced Re- and Mathematical Theory of Computation: Papers in
search Projects Agency, ARPA Order 8607, monitored Honor of John McCarthy. Academic Press.
by NASA Ames Research Center under grant NAG
2-581, by NASA Ames Research Center under grant
NCC 2-537, NSF grant CCR-8915663 and Darpa con-
tract NAG2-703.

References
Bochvar, D. A. 1972. Two papers on partial pred-
icate calculus. Technical Report STAN-CS-280-72,
Department of Computer Science, Stanford Univer-
sity. Translation of Bochvar’s papers originally pub-
lished in 1938 and 1943.
BuvaE, Saga 1992. Context in AI. Unpublished
manuscript.
de Kleer, Johan 1986. An assumption-based truth
maintenance system. Artificial Intelligence 28:127-
162.
Genesereth, Michael R. and Fikes, Richard E. 1992.
Knowledge interchange format, version 3.0, reference
manual. Technical Report Logic Group Report Logic-
92-1, Stanford University.

Nonmonotonic Logic 419