Tractable Meta-Reasoning in Propositional Logics of Belief

I. Introduction

Most knowledge based systems can perform some form of deductive reasoning on their knowledge bases, which con­ tain explicit representations of some aspect of the world. Those systems or agents are usually thought of as knowing or believing 1 some fact about the world, if they are able to deduce the fact (or, more precisely, its representation) from the knowledge base. For important tasks such as planning actions, it is generally not sufficient that agents have be­ liefs only about some application domain but also about their own knowledge. For example, only after realizing that one does not know a friend's phone number one would go about finding out what it is (see Moore [Moor80] and Konolige [Kono84] for further examples on the importance of meta-knowledge and, for that matter, meta-reasoning).

Independent of what beliefs are about, actual reason­ ing must obey certain computational constraints. For ex­ ample, resource limitations are a fact of life, and when interacting with the environment, systems can afford to spend only so much time "thinking" before they are forced to act.

We are interested in models of reasoning that give rise to good computational performance, even in the presence of meta-beliefs. In addition, these models should give a se­

mantic account of reasoning, that is, relate it to the notion of truth in a way that conforms as much as possible with our intuitions.

1 For the purposes of this paper, the distinction between knowledge and belief is not important, and we use both terms interchangeably.

The framework for our investigations are logics of knowledge and belief and their model theories, which have been convenient tools in the study of reasoning for two reasons. For one, they allow us to address meta-beliefs in a direct and elegant way. Secondly, models that pre­ dict what beliefs follow from a given set of beliefs can be viewed as a knowledge level specification of a reasoner that hll!! somehow represented those beliefs internally.

One of the best understood models of knowledge and belief is provided by pouible-worldl JemanticJ. It dates back to Hintikka [Hint62], with more recent investigations in [Moor80] and [Leve82], for example. The major prob­ lem with this approach is that it prescribes reasoning that is closed under logical implication, which is strongly be­ lieved to be computationally intractable (co-NP hard) even for propositional logics, and is known to be undecidable for first-order logic. Even on intuitive grounds, closure under logical implication has been found much too demanding for real agents, a problem often referred to as logical om­ niJcience. For example, logical omniscience has an agent believe all valid sentences, something we are more than willing to give up in return for better performance.

There are mainly two approaches that try to avoid the shortcomings of possible-worlds semantics. One essen­ tially assumes. that beliefs are sentences in some syntac­ tically specified belief Jet. Examples of such models are [Eber74] and [MoHe79]. A more sophisticated approach can be found in [Kono84]. As pointed out by Levesque [Leve84], a major drawback of this syntactic approach is the fact that the kinds of sentences believed can be quite arbitrary because they depend on the form of sentences.

The appeal of possible-worlds semantics, despite its problems, is that it avoids relying on syntactic form by defining belief with respect to the classical notion of truth. Researchers following the so-called semantic approach have therefore tried to retain these properties while at the same time avoiding logical omniscience by adopting a modified notion of truth. Levesque [Leve84] was among the first to follow this route. His model of belief employs non-standard worlds, resulting in a kind of tractable inference closely re­ lated to relevance logic [AnBe75] (see section II. for more details). Fagin and Halpern develop a logic in [FaHa85] which adds a concept of awareness of primitive propositions to the standard notion of truth 2 ·

In a model by Vardi ((Vard86)), the belief set of the syntactic approach is replaced by a set of propositions, where propositions are modelled as sets of certain states of affairs. However, this still forces an agent who believes a to believe all sentences that are equivalent to a. (For a com­ prehensive overview of models of belief in the literature, see (McAr87).)

The semantic approaches mentioned above still leave one important question unanswered, namely whether there are models that allow agents to reason with their meta-beliefs in a tractable way. Even though Vardi and Fagin and Halpern overcome the problem of logical omni­ science and allow for meta-beliefs, reasoning still appears to be intractable (see section D. for more details). On the other hand, Levesque, who does provide an efficient algorithm to determine whether certain beliefs imply oth­ ers, does not allow the agent to have beliefs about itself, precluding any form of meta-reasoning, which is a serious limitation.

The main contribution of this work is that it offers a plausible semantics for the beliefs of an agent who can hold meta-beliefs and is able to·draw inferences from them efficiently. The paper is organized as follows: in section 2 we give a general outline of the model discussing its ori­ gins and motivations. Section 3 introduces the language £ and the logic BLK. In addition to a formal semantics, proof theory, and a discussion of its properties, the main tractability result is presented. Section 4 outlines changes to the semantics that allow an agent to do some introspec­ tion on its beliefs without losing tractability (resulting in the logic BL4 ). We conclude with a short summary and an outlook on open questions and future work.

II. The Approach

The model of belief proposed in this paper is an exten­ sion of Levesque's model in (Leve84) which is derived from possible-worlds semantics (also referred to as Kripke struc­ tures).

A standard Kripke structure consists of a set of world~ and a binary acce~~ibility relation (R) between worlds. The main characteristic of a world is that it determines the truth of a global set of propositions. An agent at a world w is then said to believe a proposition p if p is true in all worlds accessible from w. This is the basic model for what is usually referred to as the logic K (see (HaMo85) or (HuCr68) for an introduction to modal logics). Restrictions on R result in models for certain introspective abilities of an agent. If R is transitive, for example, we get po~itive intro~pection, that is, if an agent believes p then it believes that it believes p (the logic weak S4). If, in addition, R is Euclidean 3 , the agent can perform negative intro~pection, that is, if it does not believe p, it believes that it does not believe p (the logic weak S5).

2 Their logic of general awareness where an agent can be aware of arbitrary sentences, however, has a strong syntactic flavour.

3 R is Euclidean iff for all w1 , w2, and W3, if w1 Rw2 and w1 Rw3,

In Levesque's work the major deviation from stan­ dard Kripke structures is the use of .!ituation~ rather than worlds. In contrast to a world, where everything is either true or false, a situation can support the truth of a propo­ sition, the falsity, both, or neither. Intuitively, only those propositions that are relevant to a situation are supported. A situation in which proposition p has both true and false support, can be interpreted as providing evidence both for the truth of p and for its falsity. An agent believes a propo­ sition p in a situation s, if p has true support in all situ­ ations ·accessible from s.· A more detailed picture of the properties of Levesque's model will follow from the discus­ sion of the logics presented in this paper, which subsume his model. Besides its attractiveness from a computational point of view, it is worth mentioning that, although im­ plication retains the usual properties, believing a implies believing (3 holds if and only if a tautologically entail.! (3. Tautological entailment was proposed by relevance logi­ cians as a more intuitive account of implication (AnBe75) . In a sense, the agent in Levesque's model believes all the relevant implications of its beliefs.

Our goal is to extend Levesque's semantics in a nat­ ural way to allow for meta-beliefs. In particular, beliefs about beliefs should have properties analogous to those that are just about the world. This means that the agent should not be logically omniscient with respect to its own beliefs, and in addition, its reasoning abilities should not be any more powerful when reasoning about itself. 5

A key feature underlying Levesque's logic is the fact that an agent on the one hand ·may have no opinion at all about some aspect of the world, and on the other hand, its opinion about something may be unrelated to an opinion about its negation. The extension we propose to this prop­ erty is to let that "something" also apply to the agent's beliefs about itself.

This is the idea: whenever the agent in a situation s wants to confirm a belief a, it does so by making sure that a is supported in all elements of some set of situations. Whenever it disconfirms a belief (3, it is because (3 is not supported by some member of a set of accessible situations. The crucial point is that the sets in both cases need not be the same. It is as if the agent is in (potentially) different modes of thinking when it comes to positive versus nega­ tive beliefs of its own. Caveat: We certainly do not want to suggest that humans actually behave like this. Rather, this is an attempt to provide a semantically motivated ac­ count for an arguably weak artificial agent. Another aim is to stay as close to traditional semantic models as possible. The only change to Kripke structures in addition to allow­ ing situations is the introduction of a second accessibility relation .R, which is used to determine negative beliefs.

then w2Rw3 .

4 Actually, since Levesque does not consider meta-beliefs, he dis­ penses with the accessibility relation altogether replacing it with a set of possible situations that are visible from any situation.

5 Both criteria are violated in the obvious extension to Levesque's logic, which simply allows nested beliefs without changing the se­ mantics. In fact, this would lead to a reasoner with the power of weak S5 with respect to meta-beliefs.

The two logics we are about to formally introduce not only capture this extended notion of explicit belief but are also able to express what is implicit in an agent's belief. Intuitively, by implicit we mean anything that one could possibly deduce given what the agent actually believes. The logic weak S5 seems to be an appropriate choice as a model of implicitness (see also [FaHa85) for a similar notion).

In their logic of awareness, Fagin and Halpern allow an agent to have beliefs about what is implicit in its be­ liefs. At this point, our model is not concerned with those issues because we view implicit beliefs as a purely exter­ nal characterization of an agent's beliefs and what follows from them. In other words, we assume that the agent does not know about the concept of implicitness (see section V. for further comments).

III. The Logic BLK

A. The Language C

The language .C we are using throughout the paper is a standard propositional language with a countably infinite set 1' of propositional letters (or atoms), the logical con­ nectives ..,, V, and /\, and two modal operators B and L. · Sentences of .C are either atoms or are constructed from other sentences, logical connectives or modal opera­ tors with the usual formation rules. The only constraint we impose is that no L may appear within the scope of a B . .Cs denotes the sublanguage of .C that does not contain Ls. In a sense, .Cs is the agent's language whereas .Cas a whole is used to talk about the agent's beliefs, what is im­ plicit in its beliefs, and the world. Sentences that contain neither B nor L are called objective. Sentences where every atom is in the scope of a B or a L are called &ubjective.

B. A Formal Semantics for BLK

Definition 1

A BLK-model i& a tuple M =< S, T, F, R, R >, where

1. S i& any &et, the &et of &ituation&
2. £. T and F map 1' into &ub&et& of S
3. R, R are binary relation& on S

,4. w E S i& a world iff

• w E T(p) {;::::} w ¢ F(p) for all atom& p
• for all s E S wRs {;::::} w.Rs
• for all worlds w1, w2 E S, and &ituation& s E S
• if w1Rw2 and w2Rs then w1Rs
• if w1Rw2 and w1Rs then w2Rs

tran&itivity

Euclidean The understanding of T and F is that if s e T(p) and t E F(p ), then s supports the truth of p and t its falsity. Since T and F map into arbitrary subsets of S, it is easy to see that this captures exactly the notion that a situation can support either the truth, the falsity, both, or neither of a proposition. As noted earlier, the accessibility relations R and R capture the intuition that an agent in a given situation s may use different sets of possible situations to confirm or disconfirm a belief. Worlds are, of course, just those situations that look like Kripke worlds. In particular, R and R coincide at a world, and as far as worlds are concerned, the model reduces to a transitive and Euclidean Kripke structure. Note that, in addition, a world can see exactly those situations (including non-worlds) that are visible to any world that can reach this world.

8 We will freely use formulas containing additional connectives like :::> and ::, where Ot :::> P and Ot ;;: P should be understood in the standard way, viz. as shorthand for (-.Ot V {3) and (0< :::> {3) A ({3 :::> 0<), respectively.

Given a model M, we can now define what it means for a situations in M to support the truth ( ~T ) or falsity ( ~. ) of any sentence in .C.

1. M, s ~T p {;::::} s E T(p) M, s ~. p {;::::} s E F(p)
2. M,s ~T ..,a {;::::} M,s ~.a M,s ~ · ..,a {;::::} M,s ~T a
3. M,s ~T a 1\/3 {;::::} M,s ~T a and M,s ~T f3 M,s ~.a 1\/3 {;::::} M,s ~.a or M,s ~. f3
4. M,s~TaV/3 {;::::} M,s~TaorM,s~Tf3'

M,s ~.a V /3 {;::::} M,s ~.a and M,s ~. f3

1. M, s ~T Ba {;::::} for all t, if sRt then M, t ~T a M, s ~. Ba {;::::} for some t, silt and M, t ~T a
2. M, s ~T La {;::::} for all worlds w, if sRw then M,w ~Ta

M, s ~. La {;::::} M, s ~T La

For a world w in M and a sentence a E .C we say that a is true in M at w if M, w ~T a; otherwise a is fal&e. A sentence a is said to be BLK-valid (written ~a) iff a is true in all BLK-models M and all worlds win M.

C. Properties of BLK

Our intuition that everything deducible given what is be­ lieved is implicit is captured by the following properties of BLK:

1. ~Ba :J La
2. ~Ba :J LBa
3. ~..,Ba :J £-,Ba
4. ~La :J LLa
5. ~-,La :J £-,La

1-3 say in essence that not only what is believed is implicit, but also the fact that it is or is not believed is implicit. Incidentally, 2 and 3 are not valid in Fagin and Halpern's logic of awareness [FaHa85). Finally, 4 and 5 indicate thp.t Lis essentially a weak S5 operator.

Concerning the behaviour of the B operator, we first look at how logical omniscience is avoided. Here we get all the properties of Levesque's logic with the following sentences being satisfiable:

It is important to note that these sentences are satisfiable even when oc and fJ are subjective sentences.

In order to get a better understanding of what kinds of explicit beliefs follow from a given set of beliefs, we first present a proof theory that is both sound and complete with respect to the above semantics:

1. Axioms for standard propositional logic.
2. r L( oc :J fJ) :J ( Loc :J LfJ)
3. r Boc :J Loc
4. r q :J Lu, where q is a subjective sentence 7
5. r Boc = BocoNP, where OtoNP is Ot converted into con­ junctive normal form (CNF)'
6. r (Boc 1\ B{J) := B(oc 1\ fJ)
7. r (Boc V B{J) :J B(oc V fJ)

Rules of Inference:

1. if r Ot and r ( Ot :J fJ), then r fJ
2. if r oc, then r Loc

Assuming the standard notion of theoremhood we have

Theorem 2 For any 1entence oc in .C, oc il a theorem of BLK if and only if oc il BLK-valid.'

From the proof theory, it is apparent that BLK restricted to sentences without nested modal operators reduces to Levesque's logic. All of Levesque's axioms appear (some­ times in a modified form) in BLK. The only new axiom and inference rule are 4 and 11, both addressing nested beliefs. Axiom 4 makes sure that L has the right weak S5

7 This axiom schema subsumes the sentences used in properties (2) - (5) of BLK above

8 Equivalently, we could have used axiom schemata that allow con­ version into CNF, for example, B(...,(aA/3));;: B(...,aV...,/3) or B(aV(/3A"f));;: B((aV/3)A(al\"()). Note that subsentences of the form B"( are treated as atomic here.

9Proofs are generally omitted for reasons of space. They appear in [Lake88) .

properties, whereas rule 11 determines what kinds of ex­ plicit beliefs follow frc;>m nested beliefs. As a consequence, if we treat sentences of the form Boc in the scope of a B as atomic, we get exactly the same relevant implications I=Boc :J BfJ as in Levesque's logic, for example:

In addition, the inference rule 11 allows the agent to per­ form relevant implications at any level provided the levels are the same on either side of the implication. Examples with beliefs at level two are:

I=BB(oc V fJ) :J BB(fJ V oc) I=BBoc :J BB(oc V fJ) I=B-.B(oc V fJ) :J B-.Boc I=BB(oc 1\ fJ) :J BBoc I=B(Boc V B{J) :J BB(oc V fJ)

D. Computational Properties of BLK

As we have already seen earlier, there are many things a reasoner using this model of belief cannot deduce. A major limitation, for example, is the inability to perform modtu ponen~. The obvious question then is whether we get any mileage out of these limitations in terms of m~re efficient reasoning. In particular, if the agent's knowledge is represented as a conjunction of sentences KB of .Cs, how hard is it then for the agent to determine whether it believes some other sentence oc, or more formally, is there a tractable (polynomial time) algorithm to decide whether I=BKB :J Boc?

Before giving the answer, let us first go back to the logic of awareness in [FaHa85] which, as was mentioned in the introduction, does not lend itself to tractability, even when KB and oc are in CNF. We can now be a little more precise about this. The problem of deciding BKB :J Boc is co-NP hard in Fagin and Halperns logic of awareness. Since the proof is straight forward, we will not introduce the logic formally, but rather give an informal argument: let KB and oc be objective sentences in CNF and, in particular, let oc = (p 1\ -.p ). Since inconsistent sentences are never believed in this logic, BKB :J Boc is true iff KB is unsatisfiable (in the classical sense), since every satisfiable (objective) sentence can be believed. Deciding satisfiability of CNF formulas is NP-complete and thus the original problem is at least as hard as the complement of an NP-complete problem, for which no known tractable solution exists. (For the other logics in [FaHa85] and [Vard86] a similar argument holds.)

For the logic BLK, the problem is in general also too hard. As was shown by Patel-Schneider in [Pate85], the problem is co-NP complete if KB and oc are arbitrary objec­ tive formulas. However, if oc and KB are in CNF, Levesque [Leve84] could show that the problem is O(IKBI x loci), where hi denotes the length of a sentence "Y· (Levesque also notes that deciding whether oc is implicit in what the agent believes is still co-NP complete.) Certainly, con­ verting a formula 1 into CNF can be exponential in hi· However, in the intended application, if the knowledge of an agent remains relatively stable, it is only a that needs to be converted into CNF, where a can be assumed to be much smaller than the KB. Also, adding a belief to the KB only involves adding the CNF-version of the new belief without touching the old KB.

In the rest of this section we will demonstrate that a result similar to Levesque's holds for BLK with the important addition that the agent can reason efficiently also about its own beliefs. Since we are allowing meta­ beliefs, we first have to introduce a slightly modified ver­ sion of CNF, which we call extended conjunctive normal form (ECNF for short).

Definition 3 A Jentence a in Cs iJ called an extended clause (e-clauJe) iff

where each ai iJ either a literal (i.e., an atom or itJ nega­ tion) or of the form B(3 or -.B(3 where (3 itJelf iJ an e­ clauJe.

Definition 4 A Jentence a in Cs iJ in ECNF iff

and every ai iJ an e-clauJe.

An example of a formula in ECNF is

Lemma 5 Every a in £a can be converted into a formula a.o'"' in ECNF Juch that

f=Ba = Ba.oNP·

The following theorem and corollary essentially give us the specification for an efficient algorithm to determine f=BKB :::> Ba if both a and KB are in ECNF:

Theorem 6 Let a and (3 be e-claweJ of the form

with ai(1 ~ i < k) and f3;(1 ~ j < n) being literalJ. Then f=Ba :::> B(3 if and only if

1. for all i , 1 ~ i < k, there iJ a j, 1 ~ j < n -'· t. ai = f3; , and
2. for all i, k ~ i < l, there iJ a j, n ~ j < o -'· t. f=Bai :::> Bf3; , and
3. for all i) l ~ i < m, there iJ a j , o ~ j < p -'· t. f=Bf3; :::> Bai

The if-direction can be proved directly by a simple argu­ ment about any BLK-model M and world w that support Ba. The only-if direction involves an induction on the number of Bs occurring in a and (3. It is not hard to see that the base case, i.e., a and (3 are objective sentences, reduces to Levesque's procedure in (Leve84). Note that we could rephrase a) as f=B v~~; ai :::> B V'l~i (3;. The proof of the only-if direction for part c) crucially depends on the fact that reasoning about explicit beliefs does not allow chaining, for example, l;lB( -.Bq) :::> B( -.Bp V -.B( -.p V q)) in contrast to f=L(-.Lq) :::> L(-.Lp V -.L(-.p V q)). In fact , from part c) we obtain the following corollary:

Corollary 7 Let a and (3 be in ECNF, where a = A ai and (3 = A (3;.

Then f=Ba :::> B(3 if and only if for each (3; there iJ an a, $UCh that f=Bai :::> B(3;.

Proof : The result follows immediately from theorem 6 and the fact that

Given the previous theorem and corollary, it is easy to see that detennining f=BKB :::> Ba with KB and a in ECNF and arbitrary nestings of beliefs is no harder than the case where only object level sentences are considered.

Theorem 8 If KB and a are in ECNF, then

f=BKB :::> Ba can be determined in time O(IKBI X lal).

Proof : The proof follows a simple induction argument on the number of Bs in both KB and a. Note that the base case corresponds directly to Levesque's result about object level beliefs. I

IV. The Logic BL4

So far, we have modelled agents that are able to reason ef­ ficiently about their own beliefs, but are only able to draw conclusions from meta-beliefs if they are explicitly repre· sented in their knowledge base. That is, they lack any introspective capability. (Implicit beliefs are, of course, introspective, but the agent does not know about them.) We will now add positive introspection to the agent's abil­ ities, which, as it turns out, does not substantially affect the computational properties of reasoning as discussed for BLK.

At first glance it seems that all one has to do is add transitivity to the R relation, which will certainly make Ba :::> BBa valid (as it does in standard Kripke struc­ tures). However, on closer inspection one notices that this alone does not preserve a nice symmetry between reasoning from positive and negative beliefs which we have in BLK, where (1): BBa :::> BB(3 is valid iff (2): B-.B(3 :::> B-.Ba is. In particular, if we replace (3 by Ba, then (1) is valid, but we can easily find models that make (2) false if the only change to the semantics is letting R be transitive. We can regain the above symmetry if we add another transitivity rule which relates both R and fl. These modifications give us the logic BL4:

Definition 9 A model M =< S,T,F,R,R > i1 a BL4model iff

M i1 a BLK-model and

• R i1 tran~itive.
• for all 1ituation1 s, t, and u, if sRt and tRu, then sRu.

A sentence o: i1 BL4-valid iff o: il true in all BL4-mode11 M and world1 w in M.

Note that for relations between worlds nothing changes, since there both R and R coincide and are already transi­ tive and Euclidean.

The algorithm to decide whether a belief in ECNF implies another in BL4 is only a slight extension of the one for BLK:

Theorem 10 Let o: and fJ be a~ in theorem 6. Then f=Bo: :::> BfJ if and only if either f=Bo: :::> BfJ; for 1ome j, n s; j < o, or Condition1 a), b), and c) of theorem 6 (with f= read a1

BL4-validity).

The following example illustrates why the new condition is needed:

We leave it to the reader to verify that this sentence is valid in BL4 but not in BLK.

The analogue of corollary 7 holds in this logic as well. With that it is not hard to show that deciding whether f=BKB :::> Bo: for KB and o: in ECNF is still polynomial time.

Theorem 11

IfKB and o: are in ECNF, then f=BKB :::> Bo: in BL4 can be determined in time O(IKBI x lo:l).

Of course, the question arises what happens if we add also negative introspection. In that case it seems that we run into trouble, both from a conceptual and a computational point of view. For one, from f=Bo: :::> BBo: and f=...,Bo: :::> B...,Bo: one can immediately infer f=B(...,Bo: V Bo:), which means that we have brought in a form of logical omniscience through the back door (at least as far as subjective sentences are concerned). Note, however, that this still allows an agent to hold inconsis­ tent beliefs about itself without believing everything. In order to determine f=BKB :::> Bo: one now has to test for the validity of Bo:, which in case of objective sentences in CNF is trivial. For formulas in ECNF we have not yet found a complete algorithm to test for validity. We conjec­ ture, however, that it is still tractable, since formulas like B[B(Bpi\(Bp :::> Bq)) :::> BBq) need not be valid, that is, there is no.obvious way of simulating propositional reason­ ing inside an ECNF.

V. Summary and Future Work

We have presented a model of explicit belief that avoids the problem of logical omniscience. The major contribution of this paper is that reasoning about beliefs in the sense of deciding f=BKB :::> B o: is tractable (assuming a certain nor­ mal form). This is true even in the case of meta-beliefs on either side of the implication. Furthermore, adding posi­ tive introspection does not change the complexity.

There are still many issues left open. One, which is probably more of theoretical interest, is how to allow the agent to know about implicitness. For example, one might want to model the property that the agent thinks it knows exactly what is implicit, i.e., one might want BBo: = BLo: and B-,Bo: = B-,Lo: to be valid. (See also [FaHa85), where Bo: = BLo: is valid in the logic of awareness.) Straight forward extensions of BLK and BL4 do not have these properties.

Other issues concern the fact that the logics BLK and BL4 are arguably very weak. For one, they have no notion of consistency, not even with respect to meta-beliefs. For example, the sentence B(p 1\ ...,Bp) is satisfiable, which is a version of G. E. Moore's famous problem (see [Hint62)). In [Lake88) we show that consistency requirements of this form can be accommodated without sacrificing tractable reasoning. Furthermore, the language C itself is not ex­ pressive enough for many knowledge representation pur­ poses. Therefore, we are now looking at first-order ver­ sions of explicit beliefs. In particular, we are investigating how the results in this paper can be combined with those in [Lake86).

Nevertheless, the logics BLK and BL4 demonstrate already that reasoning about object and meta-beliefs can be done efficiently within a reasonable semantic frame­ work.

Acknowledgements

I am indebted to Hector Levesque for his patience and enthusiasm during our weekly meetings and his comments on earlier drafts of this paper. I would also like to thank Jim des Rivieres and Diane Horton for their suggestions concerning style and contents of the paper. This work was financially supported by a Government of Canada A ward and the Department of Computer Science at the University of Toronto.