A Model of Decidable Introspective Reasoning with Quantifying-In

1 Introduction

Since agents rarely have complete information about the world, it is important for them to introspect on what they know and, more importantly, do not know. For example,

if somebody tells you that Sue's father is a teacher and you have no other information about Sue's fa­ ther, then introspection (in addition to deduction) allows you to conclude that there is a teacher and that you do not know who that teacher is, that is, as far as you know, Sue's father could be any of a number of individuals.

There have been various attempts to formalize introspec­ tive reasoning, most notably in the guise of the so-called autoepistemic logics (e.g. [18, 17]). While providing a very elegant framework for introspection, these logics have a major drawback in that they assume an ideal reasoner with infinite resources. In particular, in the first-order case, reasoning is undecidable. It is therefore of particular interest to devise models of introspective reasoning which are better suited for agents with lim­ ited resources.

For that purpose, a model of a tractable introspec­ tive reasoner was proposed for a propositional language in [12]. Since its obvious first-order extension leads to an undecidable reasoner, we proposed a modification which retains decidability in [13]. However, this proposal is still too limited since it lacks the expressiveness to deal with incomplete knowledge as exhibited in our initial exam­ ple. In particular, it does not allow us to make distinc­ tions between knowing that and knowing who because the underlying language does not provide for quantifying­ in [6], that is, the ability to. use variables within a belief 1 that are bound outside the belief. With quantifying-in, the above example can easily be expressed as (we use the modal operator B for belief)

*This work was conducted at the University of Toronto.

3xTeacher(x) 1\ .,BTeacher(x),

a sentence that should follow from an introspective KB that contains only the sentence Teacher(father(sue)).

In this paper, we extend the results of [13] by consider­ ing a language with quantifying-in and equality. It is not at all obvious whether adding quantifying-in allows us to retain a decidable reasoner. As Konolige observed [8], while introspective reasoning in classical monadic pred­ icate calculus is decidable, it becomes undecidable if we add quantifying-in. As a result, Konolige makes the fol­ lowing comment:

Thus the presence of quantifying-in seems to pose an inherently difficult computational problem for introspective systems.

In this paper we show that, given an arbitrary first-order KB, it is decidable for a large class of sentences with quantifying-in whether or not these sentences follow from the KB.

One way to formalize reasoning is to view the problem as one of modeling belief. In a nutshell, a model of be­ lief tells us what the possible sets of beliefs or epistemic states of an agent are. One then needs to specify for any given KB which epistemic state it represents. Under this view, reasoning reduces to testing for membership in the appropriate epistemic state.

As in [12, 17], we use an approach that allows us to model the beliefs of a KB directly within the logic. In­ tuitively, a KB's epistemic state can be characterized as the set of all sentences that are believed given that the sentences in the KB are all that is believed or, as we will say for short, only-believed. We formalize this idea using a modal logic with two modal operators B and 0 for belief and only-believing, respectively. This allows us to say that a KB believes a sentence a just in case OKB ::> Ba is a valid sentence 2 of the logic, thus charac­ terizing the epistemic state of the KB. The complexity of reasoning then reduces to the complexity of solving this validity problem.

1 We use the terms knowledge and belief interchangeably in this paper, even though belief is the more appropriate term, since we allow an agent to have false beliefs.

In related work, Konolige [8] also addresses the issue of modeling introspection under resource limitations. How­ ever rather than proposing an actual instance of a com­ putationally attractive reasoner, he presents a general framework in which one can be formalized. Since we consider a limited introspective reasoner who is able to perform full introspection and is only limited in his de­ ductive component, work on limited deduction alone is also relevant [7, 2, 19, 4]. In particular, as discussed in [13], [19] is a special case of ours. Finally, in prelim­ inary work [11], we proposed a model of limited belief with quantifying-in yet without nested beliefs. As a re­ sult , the corresponding reasoner was purely deductive and not able to make use of quantifying-in himself.

In the next section, we introduce the logic OBLIQUE, 3 which defines the model of belief and only­ believing. In Section 3, we take a closer look at the epis­ temic states of KB's as defined by OBLIQUE. Section 4 shows the computational pay-off of using this particular limited form of belief. In Section 5, we use the logic to define a KR service that allows a user to query a KB and to add new information to it. Finally, we end the paper with a brief summary and an outlook on future work.

2 The Logic OBLIQUE

We begin with a discussion of belief and only-believing.

Belief

As in in [13], belief is modeled by integrating ideas from possible-world semantics [5, 9] and relevance logic [1 , 3]. Roughly, an agent believes a sentence just in case that sentence holds in all states of affairs or sit­ uations the agent imagines. In order to obtain agents with perfect introspection we require that, similar to a semantics of the modal logic weak S5, that every model has one globally accessible set of situations. Situations are a four-valued extension of classical worlds. Instead of facts being either true or false, situations assign them independent true and false-support, which corresponds to the use of four truth values{}, {true}, {false}, and {true, fa).se}, an idea originally proposed to provide a semantics for a fragment of relevance logic called tauto­ logical entailment (1, 3] . 4

In order to be able to distinguish between knowing that and knowing who, we follow (17] and use a language with both rigid and non-rigid designators (see [10]). The non-rigid designators are the usual terms of a first-order language such as father(sue), which may vary in their interpretation. The rigid designators are special unique identifiers called standard names. For simplicity, the standard names are taken to be the universe of discourse in our semantics.

2 Whenever KB occurs within a logical sentence, we mean the conjunction of all the sentences in the KB.

3 Thanks to Hector Levesque, who suggested that name to me. It may b.e read as "Qnly !!elief 1ogic with Quantifiers and E.quality."

4 Levesque [16) was the first to introduce the notion of four-valued situations to model a limited form of belief in a propositional framework.

Employing four-valued situations instead of worlds has the effect that beliefs are no longer closed under modus ponens, e.g. B(p V q) and B(-.q V. r) may be true and B(p V r) may be false at the same time. As discussed in [13], a further restriction is needed in order to use this model of belief as a basis for a decidable reasoner. In particular, the link between disjunction and existential quantification is weakened in the sense that an agent may believe P(a)VP(b), yet fail to believe 3xP(x). In the case of beliefs without quantifying-in, this can be achieved semantically by requiring that an agent who believes the existence of an individual with a certain property must be able to name or .give a description of that individual. More concretely, in order to believe 3xP(x) there must be a closed term t (e.g. father(sue)) such that P(t) is true in all accessible situations (see (13]).

In the case of beliefs with quantifying-in, this idea of simply substituting terms for existentially quanti­ fied variables does not suffice. E.g., given the belief 3xTeacher(x) 1\ -.BTeacher(x), if we replace x by any term, say father(sue), then the resulting belief is in­ consistent because for an introspective agent to believe that Teacher(father(sue)) 1\ -.BTeacher(father(sue)) means that he both believes and does not believe that Teacher(father(sue)). What is wrong is that we should not have substituted father(sue) for the second occur­ rence of x (within the context of B). Instead, what we really want at its place is the denotation of father(sue) so that, while Teacher(father(sue)) holds at every sit­ uation the agent imagines, the agent does not know of the denotation of father(sue) at any given situa­ tion that he is a teacher, that is, the agent does not know who the father of Sue is. To make this distinc­ tion between a term and its denotation we introduce a so-called level marker .0 which is attached to a term whenever the term is substituted within the context of a modal operator. In our example, the substitution results in Teacher(father(sue)) 1\ -.BTeacher(father(sue).o). Later we will return to this example and demonstrate formally how the use of level markers has the desired effect. 5

Only-Believing

An agent who only-believes a sentence a believes a and, intuitively, believes as little else as possible. In other words, the agent is maximally ignorant while still believing a .

As demonstrated in [12, 17], if belief is modeled by a set of situations, independent of whether they are four­ valued or two-valued as in classical possible-world semantics, only-believing has a particularly simple charac­ terization: an agent only-believes a sentence a if he or she believes a and the set of situations M is as large as possible, i.e., if we were to add any other situation to M, the agent would no longer believe a. 6

5 ln the logic, we allow an infinite number of distinct level markers. While not apparent in this paper, this choice was made for technical convenience. The reader may simply ig­ nore all level markers other than .0.

With the special treatment of existential quantifica­ tion as outlined above, we need to pay special attention to the case of only-believing sentences that contain exis­ tential quantifiers (see also [13]). Consider the example of only-believing a = 3xP(x). Since a is believed, we need a term t such that P(t) is believed as well. How­ ever, t should not carry any information about the world (where should the information come from?). Thus t has to be a generic term much like a Skolem function.

For that reason, we introduce a special set of function symbols called sk-functions, which must be used when substituting existentials in the context of only-believing. To obtain the desired effect, we allow KB's to contain sk-functions while excluding them from epistemic states. This way, given an sk-function t,~c and a KB = P(t.~c), the beliefs that follow from KB are the same as if KB = 3xP(x).

2.1 The Languages C and BC

We introduce a language£, which allows us to talk about the beliefs of a KB and a language 8£, which is a sub­ language of C and which contains all the sentences that qualify as possible beliefs of a KB. For example, the op­ erator 0 may be used to talk about the beliefs of a KB but it may not appear within a belief itself. 7

The language C is a modal first-order dialect with equality and function symbols, which form a countably infinite set :F, which itself is partitioned into two count­ ably infinite sets :FaEG and :FsK of every arity. The latter contains the sk-functions mentioned earlier. The language also contains a countably infinite set N = { #1, #2, .. . } of standard names, which are syntactically treated like constants. Finally the level markers form a countably infinite and totally ordered set with a least element. They are written as .i, where i is a natural number. The ordering is .0 < .1 < .2 < .3 < ...

Given the usual definitions of terms, a primitive term is a term with only standard names as arguments. Given a term t, an extended term i is obtained from t by appending zero or more subterms oft with level mark­ ers such that, if u.i occurs in i, then u is not a variable and does not contain level markers. 8 Atomic formulas (or atoms) are predicate symbols whose arguments are extended terms. Primitive formulas are atoms with standard names as arguments.

The formulas of C are constructed in the usual way from the atomic formulas, the connectives ..., and V, the quantifier 3, 9 and the modal operators Band 0 . To simplify the technical presentation below, we also require that no variable is bound more than once within the scope of a modal operator of a formula. Formulas with­ out any occurrences of B or 0 are called objective, formulas without OCCUrrences of 0 are C(!.lled basic, and formulas whose predicate symbols all occur within the scope of a modal operator are called subjective. Sen­ tences are, as usual, formulas without free variables.

6 M need not be unique for the same reasons as there are multiple extensions in autoepistemic logic (see [12, 17]).

7 This restriction of BC was chosen to simplify the techni­ cal treatment. Besides, there seems to be little practical use for beliefs about whether something is all that is believed.

8 E.g., given a term f(a) (a constant), f(a.O) and /(a).14 are extended terms, but /(a).1.3 and f(a.1).14 are not.

9 0ther logical connectives like A, ::> , and=: and the quan-

The language 8£, over which the epistemic states of KB's will be defined, is a sublanguage of C and consists of all those basic formulas of C that contain neither level markers nor sk-functions. We often use the terms 8£­ formulas and 8£-sentences to refer to the formulas and sentences of BC.

Notation: Sequences of terms or variables are some­ times written in vector notation. E.g., a sequence of variables (x1, ... , x~c} is abbreviated as x. Also, 3x stands for 3x 1 . . . 3x k. If a formula a contains the free variables Xt, . . . , x~c, a[xt/t1, . .. , x~c/t~c] (abbreviated as a[xJn) denotes a with every occurrence of Xi replaced by ti. If the context is clear, we omit the variables and write a[tt, ... , t~c] or a[~ instead. The truth values true and false are used as shorthand for (#1 = #1) and (#1 :f: #1), respectively.

The following definitions are needed for the semantics of B and 0. In particular, Definitions 2 and 3 describe what terms can be substituted for the existentially quan­ tified variables when interpreting Band 0, respectively.

Definition 1 A variable occurs {is bound) at the objec­ tive level of a if it occurs {is bound) outside the scope of any modal operator in a.

Let a be a formula in C. Let x be a variable that is bound at the objective level of some formula (3 such that either (3 = a or B(J is a subformula of a. x is said to be existentially (universally) quantified in a iff x is bound within in the scope of an even (odd) number of ...,-operators in (3.

For example, in 3x-,B3yP(x, y), both x and y are con­ sidered existentially quantified.

Definition 2 Admissible Terms

Let a be a formula and x existentially quantified in a. A term t is said to be an admissible substitution for x with respect to a iff every variable y in t is universally quantified in a and x occurs within the scope of y.

If the context is clear, we often say t is admissible for x or t is admissible.

Definition 3 Sk-terms

Let a be a sentence and x an existentially quantified variable bound at the objective level of a. Let U ( x) be a sequence of the universally quantified variables in whose scope x is bound. Let f E :FsK be a function symbol of arity IU(x)l occurring nowhere else in a. Then f(U(x)) is called an sk-term {for x ).

Definition 4 Let a be a sentence and let x (x1 , . .. , x~c} be a sequence of the existentially quantified variables bound at the objective level of a. a~ denotes a with all 3xi removed.

tifier V are used freely and are defined in the usual way in terms of-., v, and 3.

Example 2.1 Let a= 3w'v'x3yP(w, z, y) 1\ B3zQ(z). Then a~= 'v'zP(w, x, y)I\B3zQ(z). Note that existential

quantifiers within modalities are left untouched.

Definition 5 Let a be a formula with free variables i = (z1, ... , ZJ:). (a may contain other free variables as well.) Lett= (t1, ... , tA:) be a sequence of terms.

a[iji) is a with every occurrence of Zi at the objective level replaced by ti and every occurrence of Zi inside the scope of a modal operator replaced by tj.O.

Example 2.2

Let a= P(z!)AB(...,Q(z!)VR(z2)) . Then a[ztfa, z2/b] = P(a) 1\ B(-,Q(a.o) V R(b.o)). Note the difference to a[ztfa, z2/b] = P(a) 1\ B(...,Q(a) V R(b)), that is, [ ... ]in­ dicates regular substitutions, while [ ... ] indicates that substitutions within modalities are appended with level marker ~0.

2.2 A Formal Semantics

We first define situations, which are a four-valued exten­ sion of classical (two-valued) Kripke worlds [9]. Situa­ tions are defined over a fixed universe of discourse, which is the set of standard names of the language. This allows us to describe the true- and false-support of predicates in terms ·Of the primitive formulas. Closed terms are interpreted by mapping them into the standard names.

Definition 6 Denotation Function

A denotation function d is a mapping from closed terms into the standard names such that d( n) = n for all n E N and d(J(t1, ... , t~c)) = d(J(d(tt), ... , d(t~c))) for all closed non-rigid terms f(t 1 , .·. , t~c). We extend d to apply to terms with level markers. If t is a closed term and .i a level marker, then d(t.i) = d(t).

Definition 7 First-Order Situations

A situation s is a triples = < T, F, d >,

where T and F are subsets of the set of primitive formu­ las and d is a denotation function .

T and F can be arbitrary sets of primitive formulas except for equality, which has a fixed interpretation, that is, (n = m) E T [(n = m) E F] iffn and mare identical [distinct] standard names.

Notice that equality has a standard two-valued interpre­ tation. The main reason why we have chosen such a strong form of equality is to obtain Theorem 2.

Definition 8 Worlds

A situation w is called a world, iff

P(n) E Tw ¢? P(n) fl. Fw for all primitive formulas P(n).

Definition 9 Let a be a sentence and s = (T,, F,, d,) a situation.

• a"' is a with every level marker .i replaced by .i-1 for all .i > .0.

a· is obtained from a by replacing every occurrence of t.O by the standard name d,(t), ift is closed, and by t otherwise.

Example 2.3 If a= P(a.O)/\ 'v'zB(Q(/(z).o)VR(g(z).1)) and s =< T,,F,,d, >with d,(a) = #1, then a'"' = P(#l) 1\ 'v'zB(Q(/(z)) V R(g(x).o)).

Note that a'"' is always well defined, since a' does not contain any occurrences of the level marker .0.

The true- and false-support for the sentences of C can now be defined. Let s = (T,, F,, d,) be a situation and M a set of situations. Let P(i) be an atomic sentence and let a and f3 be sentences except in rule 4 where a may contain the free variable z.

1. M, s FT P(i) ¢:::::> P(d,(i)) E T, M,s FF'P(i) ¢:::::> P(d,(i)) E F,
2. M, s l=T -,a <==> M, s FF a M, s FF -,a <==> M, s l=T a
3. M, s l=T a V {3 <==> M, s l=T a or M, s l=T f3

M, s FF a V f3 <==> M, s FF a and M, s FF f3

1. M, s l=T 3za <==>for some n E N, M, s l=T a[z/n]
2. M, s FF 3za <==>for all n E N, M, s I=F a[z/n] Let i = (z1, ... , ZA:) be a sequence of the existentially quantified variables bound at the objective level of a.
3. M, s l=T Ba <==> there are admissible t such that

for all s', if s' E M then M, s' l=T a'"'~ [iji)

M, s I=F Ba <==> M, s l;tT Ba

1. M, s l=T Oa <==> there is a sequence of sk-terms i;,K for i such that

for all s', s' E M iff M, s' l=T a'"'~ [i/i;;K] M, s FF Oa <==> M, s l;tT Oa

Example 2.4 Let M = { s I s FT P( a)} for some constant a. Then M FT B(3xP(x) 1\ -.BP(x)).

Proof: Let a= 3xP(x) 1\ -.BP(x). By definition, M FT Ba iff Vs E M, M, s FT a'"'~[x/t] for some admissible t. Note that, in this case, a'"' = a because a does not contain any level markers.

Then a'"'~[x/a] = P(a) 1\ -.BP(a.O). It suffices to show that for all s E M, M, s FT P(a) 1\ -.BP(a.O) . Let s = (T,, F,, d,) be any situation in M . M , s FT P( a) follows immediately from the definition of M.

To show that M, s FT -.BP(a.O), assume that d,(a) = n for some standard name n. By the definition of M, there must be a situation s' E M with a different denotation function such that s' I;CT P(n). Therefore, M,s FT -.BP(n) which implies M,s FT -.BP(a.O).

Truth, logical consequence, validity, and satisfiability are defined with respect to worlds and sets of situations. A sentence a is true at a set of situations M and a world w if M, w l=T a. a is false if M, w l;tT a. A sentence a is valid (l=a) iff a is true at every world wand every set of situations M. a is satisfiable iff -,a is not valid. 10

2.3 Quantifying-in

For sentences without quantifying-in and without level­ markers, OBLIQUE reduces essentially to the logic OBL in [13].ll For example, we obtain the same lim­ itations of belief such as no modus ponens (l;tBp 1\

10 ln this semantics, the basic beliefs of an epistemic state (represented by a set of situations) do not completely deter­ mine what is only-believed at that state. As shown in (14], this problem can be overcome. Since this issue is indepen­ dent from the main concern of this paper, we have chosen to ignore it here.

11 A minor distinction is that we allow the empty set of situations in the definition of truth and validity, while we excluded it in (13].

B(p:::) q) :::) Bq) and no existential generalization from disjunctions (j#B(P(a) V P(b)):::) B3xP(x)).

Here we focus on the additional feature of quantifying­ in, which allows us to properly distinguish between knowing that and knowing who. For example,

I=BTeacher((/ather(sue))) :::) B3xTeacher(x) while j#BTeacher((/ather(sue))) :::) 3xBTeacher(x).

In other words, knowing the non-rigid designator of a teacher (father(sue)) allows an agent to conclude only the existence of a teacher, but the agent does not nec­ essarily know who it is. On the other hand, if he knows the teacher's standard name, say #27, then he knows who the teacher is:

I=B(Teacher(f(sue)) A /(sue)= #27) ::> 3xBTeacher(x). In general, we obtain f=3xBa:::) B3xa for all a.

The Barcan formula (VxBa:::) BVxa) is not valid in general. In a sense, the agent is not able to perform ar­ bitrary universal generalization. However, if we restrict a to formulas where no existentially quantified variable is bound at the objective level of a, the Barcan formula is indeed valid. Finally, the converse of the Barcan for­ mula, f=BVxa :::) VxBa, is valid for all a.

3 Epistemic States of First-Order KB 's

Besides offering us a model of limited belief with quantifying-in, OBLIQUE specifies for every objective KB a unique corresponding epistemic state, if we take B.C to be the agent's language of belief. 12

Theorem 1 Let KB be an objective sentence. For any basic a in B.C, exactly one of f=OKB :::) Ba and f=OKB :::) -,Ba holds. 13

One important property of such epistemic states is that the question whether or not an arbitrary be­ lief follows from an objective KB reduces to the question whether an objective belief, that is a belief that itself does not mention any B 's, follows from the KB. For example, let KB = Teacher(#27) 1\ (Teacher(/ather(sue)) 1\ (father(sue) f. #27), where #27 is a standard name. Then determining the validity ofOKB:::) B(3xTeacher(x)/\...,BTeacher(x)) reduces to determining the validity of OKB:::) B(3xTeacher(x) 1\ ...,(z = #27)), that is, the formula BTeacher(x) is re­ placed by an equality expression which describes the set of all standard names who are known to be teachers. In general , it turns out that, even if the set of instances that are known to have a certain property is infinite, there is always a finite equality expression that describes it (Def­ initions 10 and 11).14

Definition 10 Let KB be an objective sentence and let a be a B.C-formula, possibly containing free variables. Let n1, ... , nm be all the standard names occurring in KB or a, and let n· be a standard name not occurring in KB ora.

12 1{ the KB is not objective, the logic may not give us a unique epistemic state for the same reasons as there are multiple extensions in autoepistemic logic [18].

13 Proofs are generally omitted for lack of space (see [14]).

14 The same process works for Levesque [17] in the case of an ideal reasoner with unlimited resources.

1. If a is closed then { true I=OKB ::> Ba RESo(KB,a) = false I=OKB ::> -.Ba 2. Otherwise let a contain the free variable x. Then (KB ) _ { V((x = n;) A RES~(KB, a~J)v RESo 'a - (1\(x # n;) A RESo(KB, a~.);")

The next definition shows how to apply RES8 recursively to all occurrences of B within a belief and thus obtain an objective belief.

Definition 11 Let KB be an objective sentence and let a be a B.C-formula.

llaiiKB n-.aiiKB lla V PIIKB ll3xaiiKB IIBaiiKB = a, for objective .a = -.naiiKs = llaiiKB V IIPIIKB = 3xllaiiKB = RESo (KB, llai!KB)

Lemma 3.1 llaiiKB is objective.

Theorem 2 Let KB be an objective sentence and a a B.C-sentence. Then f=OKB :::) Ba iff f=OKB:::) BllaiiKs·

This result is crucial in obtaining decidability results for the reasoner specified by OBLIQUE.

4 A Computational Pay-Off

While OBLIQUE specifies an admittedly weak reasoner, we gain a clear computational pay-off in return. In par­ ticular, we obtain a decidable reasoner for a large class of sentences including ones with quantifying-in. Let us call an equality expression t = t' ground if both t and t' are closed terms.

Theorem 3 Let KB = KB' 1\ E be an objective sen­ tence, where KB' contains no equality and E is a con­ junction of ground equalities and inequalities. Let a be a B.C-sentence such that every free variable x in a sub/or­ mula Br in a is universally quantified. (In other words, only universally quantified variables may participate in quantifying-in.) In addition we require that every term in an equality expression in a is either a universally quantified variable or a closed term. Then the validity of OKB :::) Ba is decidable.

Proof : (Sketch) While the proof is rather involved, it is instructive to sketch the main ideas.

First, it can be shown that we can assume, without loss of generality, that the existentially quantified variables in KB' are skolemized and KB' is in prenex conjunctive normal form.

Next, given Theorem 2, a simple induction on the nest­ ing of B's shows that I=OKB ::> Ba is decidable iff the same holds for objective a. (Note that the 11-IIKa-transformation introduces only equalities that satisfy the restrictions of the theorem.) Thus let us assume from now on that a is objec­ tive. Also, let x and fi be the existentially and universally quantified variables of a, respectively, and let a' be the ma­ trix of a (all the quantifiers removed) in conjunctive normal form.

For an objective a it is easy to see that I=OKB ::> Ba iff I=BKB ::> Ba. Next, I=BKB ::> Ba iff there are admis­ sible terms for x in a such that for all the substitutions of standard names ii E I 1 I=BKB ::> VfiB(a'[xfi))[fi/n], where I = { n I n occurs in KB or a} U { nt, ... , nj}. ·

Allowing arbitrary equalities within a KB is problematic because equality has a 2-valued semantics, which would result in hard reasoning such· as modus ponens.

On the other hand, while we have not yet proven that reasoning remains decidable if we allow arbitrary forms of quantifying-in, results in (14) strongly suggest that this is indeed the case. In any event, Theorem 3 can be used to prove the decidability of special cases such as f:OKB ::> B(3xa A -,B,B), where a and ,8 are objective formulas containing the free variable x.

5 ASK and TELL

In this section, we apply the results of this paper to the specification of a KR service in the sense of (15), which allows a user to query a KB and to add new information to it using 8£ as the interaction language.

Definition 12 ASK and TELL

Let KB be an objective sentence and a a 8£-sentence.

{ YES if f:OKB ::> BaA ...,B...,a NO if f:OKB ::> B...,a A ...,Ba ASK(KB, a)= UNK if f:OKB ::>-,BaA ...,B...,a INC if f:OKB ::> BaA B...,a

TELL(KB, a)= KB A llai!KB .

Note that the way TELLing a sentence a to a KB is han­ dled. Any occurrence of a Br within a is first evaluated with respect to the old KB and replaced by an ( objec­ tive) equality expression. Thus, if we start out with an initially empty KB0 , successive TELL-operations are guaranteed to always produce an objective KB. How­ ever, TELL is not prevented from returning a KB that lies outside the class of KB's for which reasoning is de­ cidable. A simple check would be to require that the KB is in the form KB' A E as in Theorem 3 or can be easily transformed into that form by rearranging conjuncts.

{ Teacher(jack), Teacher(jill) } KB = Emp(jack), Emp(jill), Emp(sue) Teach(jack, csc378), Teach(jill, csc484)

ASK(KB, Vx(Teacher(x) ::> Emp(x))) = UNK.

The answer is UNK because there may be teachers who are not known to the KB and who are not employees.15 ASK(KB, Vx(BTeacher(x) ::> Emp(x)) =YES.

Note the difference to the previous query. Here the KB is only asked about the known teachers.

ASK(KB, Vx(BEmp(x) ::> BTeacher(x))) = NO.

The answer is NO because Sue, who is a known em­ ployee, is not known to be a teacher.

ASK(KB, Vx(BTeacher(x) ::> 3yTeach(x, y))) = UNK.

The answer is UNK because there is no admissible term for y which would work for all known teachers. To ob­ tain the answer YES, we need to rephrase the question as Vx(BTeacher(x) :::> 3y13Y2(Teach(x, yl)VTeach(x, Y2))]. Now it is possible to substitute different admissible terms for Yl and Y2.

6 Summary and FUture Work

In this paper; we extended earlier work on limited belief by adding quantifying-in and equality. We established that reasoning is decidable if the KB is first-order and where queries can range over a large class of modal sen­ tences with quantifying-in. In the future we hope to prove the conjecture that decidability holds if we allow arbitrary forms of quantifying-in. It is also important to identify classes of sentences where reasoning is not just decidable but provably tractable as well . Finally, one should investigate to what extent modalities can be al­ lowed in the KB itself without sacrificing decidability.

15 All na.mes in KB a.re assumed to be sta.nda.rd na.mes.

Acknowledgements

I am grateful to Hector Levesque for many inspiring discussions on limited belief.