Quantifiers over Contexts

Extended Abstract

Keywords: Representation formalisms,

Representations of Belief, Intention

Tom Costello, Anna Patterson

Computer Science Department Stanford University Stanford, CA 94305

        email: {costello,annap}@cs.Stanford.EDU

Abstract

We can reason about theories, as well as in them. Many natural phenomena can be captured by theories, often by introducing a modality, true just of the theory. Rather than treat these phenomena as the sentences true in this modality, we can treat the entire theory or modality as an object. This point of view was proposed by McCarthy, who proposed calling these reified modalities contexts.

Contexts, viewed as theories or modalities, have structural properties, and associated natural structural operations, such as union and intersection. These structural properties are most naturally captured by an algebra, reminiscent of relation or dynamic algebra , a set of operations that can be applied to contexts to form new contexts.

Thus we can have a larger space of modalities than just those that are explicitly named. We add quantifiers that range over modalities, so that we can state propositions like, “no context with the property P exists”, or “all contexts obey Q”. We give an axiomatization of these quantifiers which we show is complete with respect to a natural semantics.

1 Putting Modalities Together

1.1 Modalities

Modal operators are widely used to capture intensional aspects of knowledge, belief, temporality and action. They capture the notion that there may be different viewpoints from which a particular structure can be viewed. These different vantage points can be agents beliefs, points in time, differing stages of knowledge, or different contexts.

A unifying semantics for these notions was proposed by Kripke. The essential idea is that a new syntactic operator, □, is semantically modeled by a set of possible worlds, W, and an accessibility relation on worlds R. Each world is given an assignment to propositional atoms^{1}, and the truth conditions for □ϕ at a world w, are defined as the truth of ϕ in all accessible worlds.

A natural extension to this idea is to allow more than one modality. One popular use of this is to have modalities of the beliefs of each member of a set of believers, (Halpern 1995) provides a recent overview of this approach. It is then customary to label each modal operator with a subscript to distinguish them. If □_{Sally} denotes the beliefs of Sally, and □_{Harry}, the beliefs of Harry, then if Sally believed that Harry believed that Sally Liked Harry, we would write, □_{Sally}□_{Harry}Likes(Sally, Harry).

1.2 Making new modalities from old

In this paper, we ask what modalities should exist, given that we already have a certain set of modalities. Thus, we differ from previous work on indexed modalities in that we are interested in making new modalities, not in stating facts that require multiple modalities for their expression.

We can imagine that we have the two modalities □_{Sally} and □_{Harry} that we considered earlier. It seems obvious that there is a set of beliefs that they share. This set of beliefs seems to be a well behaved modality. Other modalities are the union of the beliefs, the propositions they do not believe, and many others.

1Alternately, each world can have an associated first order structure, or a non-standard semantical structure, such as a three valued model. The choice of a propositional valuation is for simplicity, most of results extend to richer valuations.

One way of posing the question of what other modalities might exist, is to ask “What would a system that quantified over modalities look like?” We first present a simple system that allows us to quantify over modalities, but gives us no way to generate new modalities. We then look at natural ways to generate more modalities, using some notions from relational algebra.

1.3 Identity conditions on modalities

As well as a theory of what modalities exist, we also need an identity criterion for modalities. We take the most obvious criterion, extensionality. That is, we consider two modalities equal if they agree on all sentences.

c = c′ =^{def} for all ϕ.□_{c}ϕ ≡ □_{c′}ϕ

We consider what structural properties this decision has on the underlying relations. We show it identifies all bisimilar models.

1.4 Plan of Paper

We first look at Kripke models, which provide the basic model theory of modalities.

We give a sound and complete axiomatization for arbitrary universes of relations. This gives a simple system which allows quantification over modalities, but which does not have any closure conditions on what modalities should exist.

We then suggest three operators that make new modalities from old modalities. Therefore our universe of modalities will include all modalities definable using these operations. We give an axiomatization of these operators that we show is sound and complete for universes that include all first order definable modalities. This shows that these three operators are sufficient to define all first order definable modalities.

To prove this theorem we have to characterize all first order definable modalities. We consider when the modalities Kripke models define are equivalent. This needs the notion of bisimulation. We then look at what functions on the relations in Kripke models give rise to functions on modalities. We then prove a theorem which characterizes the first order definable functions on relations that give rise to functions on modalities. We show that the syntactic class of first order definable functions on modalities can be captured by our three operations on modalities.

We conclude by looking at previous related work in AI, and suggesting some natural uses for the operators we have introduced.

2 Modalities and Relations

We now state the standard definitions of Kripke structures, and review how Kripke models can give a semantics to a normal modality.

2.1 Kripke Models

We define propositional modal languages in the usual way.

Definition 1 A propositional modal language over a set P of propositional atoms is the smallest set of formulas containing each element of P, and ¬φ, φ ∧ ψ, □φ, where ϕ and ψ are formulas.

We can define the other propositional connectives, ∨, →, ≡, and the modal operator ◇ϕ = ¬□¬ϕ in the usual way.

Definition 2 A Kripke structure for propositional modal logic over a set P of propositional atoms is a triple ⟨W, R, V ⟩ where W is a non-empty set (the set of worlds), R is a binary relation on W and V is a function assigning to every world a set of propositional atoms from P.

Definition 3 The satisfaction relation ⊧ for K = ⟨W, R, V ⟩, a Kripke structure over a set of propositional atoms P is a relation between worlds and modal formulas. We define this relation inductively over the structure of a formula. Thus, for any w ∈ W,

w, K ⊧ p  ≡  p ∈ V (w)
w, K ⊧ ¬φ ≡  it is not the case that w, K ⊧ φ
w, K ⊧ φ ∧ ψ ≡  w, K ⊧ φ and w, K ⊧ ψ
w, K ⊧ □φ ≡ ∀w′ ∈ W such that w R w′, w′, K ⊧ φ

Definition 4 Let K = ⟨W, R, V ⟩ be a Kripke structure, then a formula φ is satisfied in K if and only if ∃w ∈ W. w , K ⊧ φ. A formula φ is valid in K, written K ⊧ ϕ, if and only if ∀w ∈ W. w , K ⊧ φ. A formula φ is valid if and only if φ is valid in all Kripke structures.

3 Quantificational Modal Logic

We look at quantifying over modalities in a modal logic. For simplicity, we look at the propositional case, and the modal logic K, with multiple modalities. We need to extend our language to allow modal variables, which we write as subscripts, as in ◇_{x}. We write modal constants as similarly, ◇_{c}, for the constant c. We do not allow quantification over objects, our language is propositional. We do not allow quantification over propositions, our language is not second order in this respect. Our only quantifiers are over modalities or contexts.

We also have an alternate notation, ist(c, ϕ), where c now plays the role of a modal variable or subscript. This allows a more traditional syntax in some respects.

3.0.1 Syntax

The symbols of our language L_{ℂ,ℙ} are, a countable set of propositional letters ℙ, connectives, ∧ and ¬, the symbols □ and ◇, a countable set of modal constants ℂ, parentheses ) and (, a countable set of modal variables x_{i}, y_{i}, i ∈ ω, and the quantifier ∀. We use ϕ → ψ as an abbreviation for ¬(ϕ ∧ ¬ψ) as usual.

The formulas of our language are the smallest set containing

• All propositional letters, ℙ.

• If ϕ and ψ are formulas, then (ϕ ∧ ψ) and (¬ψ) are formulas.

• If ϕ is a formula, and i is a modal constant, or a modal variable, then (□_{i}ϕ) is a formula.

• If ϕ is a formula, and x is a modal variable, then (∀x.ϕ) is a formula.

In the above definition, the formulas ϕ and ψ are sub-formulas of the resulting formula, furthermore, the property sub-formula is transitive. We say an occurrence of a variable x is bound in a formula ϕ, if it is contained in a sub-formula of ϕ, of the form ∀x.ψ. We assume variables are renamed to avoid clashes in the usual way. We say an occurrence of a variable x is free in a formula if it is not bound. We call a formula with no free variables a sentence.

3.1 Semantics

The semantics of modal logic is based around a set of worlds, and a set of binary relations over worlds. Every modality is associated with a relation, which we call its accessibility relation. We also have a valuation function, that is a function that assigns a set of propositional atoms to each world.

The semantics of a modal quantified logic, over a language L_{ℂ,ℙ} are as follows.

Definition 5 Given a language L_{ℂ,ℙ} and W a set of worlds, V a valuation function that assigns a subset of the propositional letters ℙ to each world, U a set of binary relations on worlds, and A an assignment function from modal variables and constants to elements of U, we define w, ⟨W, V, U, A⟩ ⊧_{∀} ϕ by induction on the formulas of L_{ℂ,ℙ} as follows. Let S = ⟨W, V, U, A⟩.

w, S ⊧_{∀} p  ≡ p ∈ V (w)
w, S ⊧_{∀} ϕ ∧ ψ ≡ w, S ⊧_{∀} ϕ and w, S ⊧_{∀} ψ
w, S ⊧_{∀} ¬ϕ ≡ w, S |̸=_{∀} ϕ
w, S ⊧_{∀} □_{i}ϕ ≡ ∀w′.A(i)(w, w′) implies w′, S ⊧_{∀} ϕ
w, S ⊧_{∀} ∀x.ϕ ≡ ∀R ∈ U.w, ⟨W, V, U, A[R/x]⟩ ⊧_{∀} ϕ

where A[R/x] is the assignment that is like A, except for the possible difference that it assigns the relation R to the variable x.

We have placed no restrictions on the universe of relations U. We now ask the question, what relations should be included in the universe U.

3.2 Just constants

We can follow the lead of first order logic, and consider possible all domains of relations. This is obviously wrong, if we consider relations as something that can be constructed from other relations using natural operations. It does not take account of the fact that relations which are not named by constants might exist.

However, as a starting point, we give an axiomatization of the case where there is no restriction on the universe of relations. We say Γ ⊧_{∀} ϕ, read, ϕ is a valid consequence of Γ, if, for all models 𝕄 = ⟨W, V, U, A⟩ and worlds w in W, verifying each formula in Γ, it is the case that w, 𝕄 ⊧_{∀} ϕ.

3.2.1 Axiomatics

The following are the axioms and rules of our minimal system, which we call ∀. We assume a Gentzen style system for concreteness.

All valid principles of propositional logic

⊢ □_{i}(ϕ → ψ) → (□_{i}ϕ → □_{i}ψ) Modal Distribution

\frac{⊢ ϕ}{⊢ □_{i}ϕ} Necessitation

\frac{Γ ⊢ ψ}{Γ ⊢ ∀x.ψ}

provided that x does not occur free in Γ

\frac{Γ ⊢ ∀x.ψ}{Γ ⊢ ψ[i/x]} where ψ[i/x] is the result

of freely substituting each free occurrence of x by i

We define logical derivation in the standard way, and denote it ⊢_{∀}. We now show soundness and completeness for the basic case.

Theorem 6 If ϕ is a sentence in L_{ℂ,ℙ}, then ⊢_{∀} ϕ implies ϕ is valid.

The full paper contains the proof of this theorem.

Theorem 7 If ϕ is a sentence in L_{ℂ,ℙ}, ℂ, ℙ countable, and Γ is a set of sentences of L_{ℂ,ℙ}, where Γ ⊧_{∀} ϕ, then Γ ⊢_{∀} ϕ

The full paper contains the proof of the theorem.

3.3 All un-nested modal formulas

A natural way to look at the possible universes of modalities is to consider what operations on modalities should exist. A simple way of making modalities is to make a modality from a formula. If B is a modal propositional formula without modalities then we can define ◇_{i:B?}ϕ, as

◇_{i:B?}ϕ ≡ (◇_{i}ϕ) ∨ B  (1)

Other ways of defining new modalities suggest themselves. Perhaps the most natural of these is to allow the definition of a new modality in terms of old modalities and union.

Thus, given modalities, ◇_{1} and ◇_{2}, we can allow ourselves to make new modalities as follows,

◇_{1∪2}ϕ ≡ ◇_{1}ϕ ∨ ◇_{2}ϕ  (2)

However, it is worthwhile noticing that

◇_{1∩2}ϕ ≡ ◇_{1}ϕ ∧ ◇_{2}ϕ

does not define a new modality, nor does

◇_{−1}ϕ ≡ ¬◇_{1}ϕ.

The second can be shown by noting that ¬◇_{1}¬(p ∨ ¬p) is equivalent to □_{1}p ∨ ¬p, which is valid by necessitation. Therefore ◇_{−1}¬(p ∨ ¬p) is true for all modalities ◇_{1}, but we have that ¬◇_{−1}¬(p∨¬p), a contradiction, showing that the above definition renders the system inconsistent.

The definition of ◇_{1∩2} does not define a modality unless ◇_{1}ϕ → ◇_{2}ϕ or vice-versa. In this case it yields the stronger. If there is a ϕ such that ◇_{1}ϕ ∧ ◇_{2}¬ϕ, then we have ◇_{1∩2}ϕ ∨ ¬ϕ but not ◇_{1∩2}ϕ or ◇_{1∩2}¬ϕ, which is inconsistent with modal distribution.

3.4 Nested Beliefs

Another natural operation to add is to allow nested modalities in the defining formula. Thus we could allow the definition of a modality corresponding to Sally’s opinion of Harry’s beliefs.

◇_{x;y}ϕ ≡ ◇_{y}◇_{x}ϕ  (3)

This system corresponds to the universe of relations being closed under union, union with the worlds that satisfy a property, and relational composition. The composition of two binary relations R and S, is defined as , ∀x y.R; S(x, y) ≡ ∃z.R(x, z) ∧ S(z, y).

We call the derivability relation with these new axioms 1, 2 and 3 ⊢_{∀ ∀ ∀}.

We can define a new consequence relation ⊧_{∀ ∀ ∀}. This adds the obvious clauses for ◇_{i:p?}, ◇_{x∪y} and ◇_{x;y}.

\begin{aligned}w, S ⊧_{∀ ∀ ∀} ◇_{i:p?} & ≡ & w, S ⊧_{∀ ∀ ∀} ◇_{i}ϕ ∨ p \\ w, S ⊧_{∀ ∀ ∀} ◇_{x∪y} & ≡ & w, S ⊧_{∀ ∀ ∀} ◇_{x}ϕ and w, S ⊧_{∀ ∀ ∀} ◇_{y}ϕ \\ w, S ⊧_{∀ ∀ ∀} ◇_{x;y} & ≡ & w, S ⊧_{∀ ∀ ∀} ◇_{y}◇_{x}ϕ \end{aligned}

We say ⊧_{∀ ∀ ∀} ϕ, read, ϕ is a valid under ⊧_{∀ ∀ ∀}, if, for each world w in W, and for all models 𝕄 = ⟨W, V, U, A⟩, w, 𝕄 ⊧_{∀ ∀ ∀} ϕ, where the set U is closed under all first order definable functions f from relations to relations, such that the induced map g(⟨W, R, V ⟩) = ⟨W, f(R), V ⟩ is a function on modalities.

Theorem 8 If ϕ is a sentence in L_{ℂ,ℙ}, then ⊢_{∀ ∀ ∀} ϕ implies ϕ is valid under ⊧_{∀ ∀ ∀}.

The full paper contains the proof of this theorem.

Theorem 9 If ϕ is a sentence in L_{ℂ,P}, ℂ, P countable, and ⊧_{∀ ∀ ∀} ϕ, then ⊢_{∀ ∀ ∀} ϕ

The full paper contains the proof of this theorem. The proof relies on some technical material about what constitutes a function on modalities that is presented in the next section. In particular we need to show that every first order definable function on modalities is representable by our three operations, union, composition and i: B?.

3.5 Bisimulation

We now introduce a notion, bisimulation, that we will use to define equality of modalities. In order to relate the syntactic question of when two modalities are true of the same formulas to the semantic question of a relation between accessibility relations we consider bisimulation.

Van Benthem showed the close connection between bisimulation (or more precisely p-morphisms) and definability in modal logics (1983). Using the classical transformation of modal formulas to first order formulas, he showed that a first order formula is preserved under bisimulation exactly when it is equivalent to the translation of a modal formula. We use this result to determine when the two Kripke models are extensionally equal. A key part of checking that a function on relations lifts to a function on modalities is reconising that equals are sent to equals.

Definition 10 Let K = ⟨W, R, V ⟩ and K′ = ⟨W′, R′, V′⟩ be two Kripke structures over P, then K is bisimilar to K′, K \underline{↔} K′, if there is a relation S ⊆ W × W′ such that

• ∀w ∈ W ∃w′ ∈ W′ such that w S w′, and

• ∀w′ ∈ W′ ∃w ∈ W such that w S w′, and

• x S y implies V (x) = V′(y), and

• x S y implies ∀x′ ∈ W. x R x′ → (∃y′ ∈ W′. y R′ y′ ∧ x′ S y′), and

• x S y implies ∀y′ ∈ W′. y R′ y′ → (∃x′ ∈ W. x R x′ ∧ x′ S y′).

This notion of bisimulation captures exactly that two models agree on all modal sentences.

Theorem 11 ((Benthem 1983)) For any bisimulation between two Kripke models, M, N, if M \underline{↔} N then M ⊧ ϕ if and only if N ⊧ ϕ for all modal formulas ϕ.

We use this theorem in the next section as our identity condition on first order relations. We need the identity condition on relations that correspond to extensionally equal modalities, as we wish to consider what functions on modalities exists, in terms of the functions on relations.

Thus Kripke structures agree on all modal formulas if and only if they are bisimilar. Thus any function on from Kripke structures to Kripke structures is a function on modalities if and only if it maps bisimilar structures to bisimilar structures.

3.6 First order translations

The propositional modal language we have introduced may be embedded into first order predicate logic, by the following standard translation, where [y/x]φ is the result of replacing all free occurrences of x by y in φ.

(p)^{∗}  = P x
(¬φ)^{∗} = ¬(φ)^{∗}
(φ ∧ ψ)^{∗} = (φ)^{∗} ∧ (ψ)^{∗}
(□φ)^{∗} = ∀y(R(x, y) → [y/x](φ)^{∗}) for some new variable y

In fact, only two variables are needed. We then have the following theorem.

Theorem 12 ((Benthem 1983)) A first order formula is (equivalent to) a translation of a modal formula if and only if it is invariant for bisimulation.

In the next section we use this theorem to show that our new operators can define all first order modalities.

3.7 Definable Relations

We now ask what definable functions f on relations give rise to functions on modalities g(⟨W, R, V ⟩) = ⟨W, f(R), V ⟩). If we define a new Kripke model, by generating a new binary relation on worlds, when does this definition map Kripke models that have the same theory to Kripke models with them same theory?

The answer to this can be derived from the previous theorem—the only formulas that are invariant for bisimulation are those that are equivalent to modal formulas. In this case it suffices to be able to find a formula ψ such that ⟨W, R′, V ⟩ ⊧ ◇ϕ if and only if ⟨W, R, V ⟩ ⊧ ψ(ψ).

Theorem 13 Let R be a binary relation on a set of worlds W, let v range over valuations on a set of propositional letters p_{1}, …, p_{n}, and let P_{1}, …, P_{m} be unary predicates on W, such that (p_{i})^{∗} = P_{i}(x).

For all S ⊂ W × W,

∀v.⟨W, S, v⟩\underline{↔} ⟨W, R, v⟩ implies ∀v.⟨W, ϕ(R), v⟩\underline{↔} ⟨W, ϕ(S), v⟩,

if and only if, there is a modal formula ψ, in the modal language with letters p_{1}, …, p_{n}, q, such that

(ψ(q))^{∗} ≡ ∃y.ϕ(R)(x, y) ∧ Q(y)

where q is a new propositional letter, with (q)^{∗} = Q(x).

Further, ψ can be chosen so that every occurrence of q in ψ(q) is scoped by an even number of negations, and ∧ does not occur outside any modalities that bind q.

The full paper contains the proof of this theorem.

Thus we have shown that the first order definitions of functions from Kripke models to Kripke models that are functions on modalities are exactly those that are definable using our three operations x; y, x ∪ y and x: B?.

4 Other Work

McCarthy (1993) introduced the notion of a context as a formal object. He argued that contexts should objects in a theory. This led him to introduce the modality, ist(c, ϕ), which states that a formula ϕ is true in a context c.

McCarthy saw contexts as capturing the unstated features of an utterance. He thought these features could be made more explicit by showing how contexts were related. His proposal was to characterize these relations by writing sentences that relate one context to another, lifting axioms. If ϕ being true in a context c implied that ψ was true in a context c′, he would write, ist(c, ϕ) → ist(c′, ψ).

While McCarthy was developing the idea of contexts a student of his, Guha (1991) applied the ideas to Cyc (Lenat 1995).

Giunchiglia (1993) introduced the notion of a multi-language system. Based on intuitions from proof theory, this attempts captures how patterns of reasoning in different languages can be integrated. Giunchiglia et al. (1993) address issues of non-omniscient belief, while our contexts are all logically closed. Clearly there is a clear relationship between how patterns of reasoning are related, and theories are related.

Montague (1963) showed that modal logic cannot be mimiced by a quoting machinery if the underlying language is sufficiently powerful. Attardi and Simi (1995) have developed a system that avoids these problems. They call their syntactic modalities, viewpoints.

Montague (1970) considers introducing modalities as objects. Naturally, his modalities are non-extensional. This led him away from considering structural properties, as his interests lay in the application of these ideas to natural language.

Ohlbach, while looking at more efficient ways of reasoning in modal logics (Ohlbach 1988), considered representing modalities in a first order language by reifying the worlds, and explicitly introducing the accessibility relation. This led him to consider context logics (Ohlbach 1989). His interest lay mainly in the extra expressive power this gave over standard modalities.

Shoham (1991) considered a class of modal operators each of which characterized a context. Buvač Buvač and Mason (1995) have looked at modal logics with these operators and the additional assumption that each operator has complete information about how the other operators behave. That is, their systems assume, □_{1}□_{2}ϕ ∨ □_{1}¬□_{2}ϕ. This axiom does not seem justified, even for the applications they consider. There is no reason why a database should have complete information about the contents of other databases.

Buvač (Buvač 1994) has investigated decidability, while (Massacci 1996) has considered complexity for a certain fragment.

(Buvač 1996) considers a simple notion of quantification over contexts in , which corresponds to our first completeness theorem, with the assumption □_{1}□_{2}ϕ ∨ □_{1}¬□_{2}ϕ, and a 5 like assumption that multiple modalities may always be reduced to a single modality.

Similar systems to this (Gabbay and Nossum 1997) based on fibring one logic over another (Gabbay 1996) have been proposed. (Nossum 1997) gives some decidability results. (Akman and Surav 1996) provides a survey of formal approaches to contextual reasoning.

5 Conclusion and Applications

We have presented a sound and complete model theory for a quantificational logic of contexts. We include operations that allow us to take the union of contexts and union of a context with a given statement. These operations are very natural in combining knowledge sources, and considering the knowledge in common of different sources.

The most natural operations on theories or modalities are the union of two modalities. We often want to combine theories.

The product of two modalities, created by relational composition naturally models the beliefs that one agent has about another. New modalities of this sort are natural when we consider multiple agents.

The notion of B? or adding the B worlds to what is considered possible has clear applicability in adding facts to a given theory. Let the theory true of □_{c} be axiomatized by Γ, then the theory of □_{c:B?} is axiomatized by Γ∧¬B. This operator allows us to add facts to a theory.

References

Akman, V., and M. Surav. 1996. Steps toward formalizing context. AI Magazine 17(3):55–72.

Attardi, G., and M. Simi. 1995. A formalization of viewpoints. Fundamenta Informaticae 23(3).

Benthem, J. v. 1983. Modal Logic and Classical Logic. Naples: Bibliopolis.

Buvač, S. 1996. Quantificational logic of context. In Proceedings of the Thirteenth National Conference on Artificial Intelligence.

Buvač, S., V. Buvač, and I. A. Mason. 1995. Metamathematics of contexts. Fundamenta Informaticae 23(3).

Buvač, V. 1994. Decidability of contextual reasoning. In Proceedings of the Twelfth National Conference on Artificial Intelligence.

Gabbay, D. 1996. Fibred semantics and the weaving of logics: Part I: Modal and intuitionistic logics. Journal of Symbolic Logic 61(4):1057– 1120.

Gabbay, D., and R. Nossum. 1997. Structured contexts with fibred semantics. In Proceedings of the International and Interdisciplinary Conference on Context.

Giunchiglia, F. 1993. Contextual reasoning. Epistemologia, special issue on I Linguaggi e le Macchine XVI:345–364.

Giunchiglia, F., L. Serafini, E. Giunchiglia, and M. Frixione. 1993. Nonomniscient belief as context-based reasoning. In Proceedings of the Thirteenth International Joint Conference on Artificial Intelligence.

Guha, R. V. 1991. Contexts: A Formalization and Some Applications. PhD thesis, Stanford University.

Halpern, J. 1995. Reasoning About Knowledge: A Survery. In D. Gabbay, C. Hogger, and J. Robinson (Eds.), Handbook of Logic in Artificial Intelligence and Logiuc Programming, Vol. IV, 1–34. Clarendon Press, Oxford.

Lenat, D. B. 1995. Cyc: A large-scale investment in knowledge infrastructure. Communications of the Association for Computing Machinery 38 (11).

Massacci, F. 1996. Contextual reasoning is NP-complete. In Proceedings of the Thirteenth National Conference on Artificial Intelligence.

McCarthy, J. 1993. Notes on formalizing context. In Proc. Thirteenth International Joint Conference on Artificial Intelligence (IJCAI ’93).

Montague, R. 1963. Syntactical treatments of modality, with corollaries on reflexion principles and finite axiomatizations. Acta Philosophica Fennica 16:153–167.

Montague, R. 1970. Universal grammar. Theoria 36:373–398.

Nossum, R. 1997. A decidable multi-modal logic of context. Hia skriftserie, Agder College, Norway.

Ohlbach, H. J. 1988. A Resolution Calculus for Modal Logics. PhD thesis, Kaiserslautern.

Ohlbach, H. J. 1989. Context logic. Technical report, Kaiserslautern.

Shoham, Y. 1991. Varieties of context. In V. Lifschitz (Ed.), Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy. Academic Press.