A Tractability Result for Reasoning with Incomplete First-Order Knowledge Bases

1 Introduction

As argued in [Levesque, 1998], there is only one deductive technique efficient enough to be feasible on knowledge bases (KBs) of the size seemingly required for common-sense rea­ soning: the deduction underlying classical database query evaluation. And yet, databases by themselves are too re­ stricted to serve as the representational scheme for common­ sense reasoning, since they require, among other things, com­ plete knowledge of the domain. Levesque proposed a gener­ alization of databases called proper knowledge bases, which allow for a limited form of incomplete knowledge. Despite the limitations, however, the deduction problem for proper KBs is no longer even decidable. Levesque proposed an al­ ternative reasoning procedure V for proper KBs that was logi­ cally sound and, when the query was in a certain normal form, logically complete. Moreover, he argued that it should be possible to implement V for very large KBs using database techniques. However, no proof was given.

In this paper, we examine proper KBs and the V procedure more closely, and we prove a tractability result for this type of logical reasoning that are comparable to those that exist for classical database query evaluation. In particular, we adapt a bottom-up database retrieval algorithm to the case of proper KBs. Thus, what we show here is that in some cases it is indeed possible to reason efficiently with incomplete knowl­ edge in a logically sound and complete way, or at least as efficiently as we can with a database.

The rest of the paper is organized as follows. In the next section, we review proper KBs and V, prove a new property of V, i.e. locality, and define answers to open queries. In Section 3, we review the complexity of database query evalu­ ation, and present a polynomial time algorithm for evaluating k-guarded formulas. In Section 4, we show how to use this al­ gorithm to evaluate queries wrt proper KBs and hence obtain a tractability result. In Section 5, we illustrate this query eval­ uation method for proper KBs with some example queries. Finally in Section 6, we describe some future work.

2 Proper KBs and V

2.1 Basic definitions

We use a standard first-order logical language£ with a count­ ably infinite set of constants C = { c1 , c2 , ... }, no other func­ tion symbols, and a distinguished equality predicate. We have in mind that in any interpretation, = should be understood as identity, that the constants will be unique names. This can be captured by a set of axioms £, consisting of the axioms of equality and the set of formulas {ci =J Cj I i =J j}.

In what follows, p ranges over atoms (excluding equality) whose arguments are distinct variables; e ranges over ewffs, i.e. quantifier-free formulas whose only predicate is equal­ ity. 't/a denotes the universal closure of formula a; ad de­ notes a with all free occurrences of x replaced by constant d. The width of a is the maximal number of free variables in its subformulas. The quantifier rank qr(a) of a is the depth of nesting of quantifiers in a.

Definition 2.1 A KB ~ is proper if£ U ~ is consistent and~ is a finite set of formulas of the form 't/(e :J p) or 't/(e :J -.p).

To illustrate the idea of a proper KB, imagine a scenario in­ volving a robot security guard keeping track of the occupants of the rooms of a building. The robot can find out that some­ one has entered or left a room, and by going into a room, find out who the occupants are. We can express what the robot might know using a proper KB: 1

• Alice is alone in Room 1.

't/xy. x =alice 1\ y =room] :J ln(x, y) 't/xy. x =alice 1\ y =J room] :J -.Jn(x, y) 't/xy. x =J alice 1\ y =room] :J -.In(x, y)

1 We think of these as beliefs about some initial state of the world. It should be possible to generalize the notion of proper KB to deal with state change. See Section 6 for discussion.

• Bob and possibly others are in Room 2. Vxy . x = bob 1\ y = room2 :J In(x, y)
• Vxy. x = bob 1\ y-/=- room2 :J --,fn(x , y )
• Carol is not in the building.
• Vxy . x =carol :J --,Jn(x, y )
• Only Bob and Carol go into Room 3. Vxy. x-/=- bob 1\ x -/=- carol /\ y = room3 :J ·ln(x, y)

Note that this information cannot be expressed in a traditional database where, e.g. we cannot leave open the occupants of Room 2. On the other hand, facts requiring disjunction or ex­ istential quantification cannot be expressed as part of a proper KB, e.g. every room having at most three occupants.

It is not hard to see that the problem of determining whether a sentence is logically entailed by a proper KB is undecidable, since when the KB is empty, this reduces to classical validity. 2 Levesque [1998] proposed the reasoning procedure V instead. Given a proper KB and a query, V re­ turns one of three values 0 (known false) , 1 (known true), or ! (unknown) as follows:

1. V[E, t = t'J = 1 ift is identical tot', and 0 otherwise;

1. V[E,3xa] = max{V[E, ad] I d E H+(E U {a})}, where H+(S) is the union of the constants inS, and a constant not inS, say the lexicographically smallest one.

This V procedure always terminates, and is logically sound (i.e. if it returns 1 (resp. 0), then the query (resp. its negation) is logically entailed by£ U E). Moreover, Levesque defined a certain normal form called NF, and proved that for queries in NF, the V procedure is also logically complete (so that, for instance, V returns 1 iff the query is logically entailed). Fi­ nally, Levesque showed that in the propositional case, every query could be equivalently expressed in NF, and conjec­ tured that this was also true in the first-order case.

2.2 Invariance under renaming

The first difficulty that arises when attempting to reason with proper KBs is the fact that unlike with databases, we cannot fix the domain in advance, or even put an upper bound on its size. For example, if E consists of just Vx(x -/=-a :J P(x)), and an is the sentence of .C that says that there are at least n distinct instances of P, then V[E, an] = 1 for all n. However, we can take advantage of the fact that for this E, all constants other than a behave the same. This will allow us to define finite versions of answers to open queries, as shown below. Notation Let a be a formula and S a set of formulas. Let * be a bijection from C to C. We use a* to denote a with each c replaced by c*, and use S* to denote {a* I a E S}.

2 The classical validity problem is undecidable even when there are no function symbols.

Lemma 2.2 Let e be an ewff, and let * be a bijection from C to C. Then£ f= e iff£ f= e*.

Theorem 2.3 Let E be a proper KB and a a sentence. Let * be a bijection from C to C. Then V[E, a ] = V[E*, a* ].

Proof: The proof is by induction on the structure of a. The case for atoms uses Lemma 2.2. The cases for equalities, negations and disjunctions are trivial. Now consider 3xa. Let d E H+ (E U {a }) . If d appears in E or a, by induction, V[E, a d] = V[E*, (ad)*] = V[E*, (a*)d. ]. Otherwise, d* does not appear in E* or a* . Now let c E H+ (E* U {a* }) such that c does not appear in E* or a*. Let* be the compo­ sition of * and the bijection that swaps c and d* and leaves the rest constants unchanged. Then d* = c; E* = E*, a* = a* , since neither d* nor c appears in E* or a*. By induction, V[E, a d] = V[E* , (a *)d, ] = V[E*, (a*)~] . Thus V[E, 3xa] = max{V[E, ad] I d E H+ (E U {a})}= max{V[E*, (a*)d] I dE H+(E*U{ a*} )}=V[E*, (3xa)*]. ·

Corollary 2.4 Let E be a proper KB and a a f ormula with a single free variable x . Let c and d be two constants that do not appear in E or a . Then V[E, a~ ] = V[E, ad].

Proof: Follows from the theorem by taking * as the bijection that swaps c and d and leaves the rest constants unchanged. ·

2.3 Locality

A nice property of V is its locality, i.e., for any proper KB E and query a, the value of V[E, a ] only depends on those sentences of E that mention some predicate in a.

Definition 2.5 Let E be a proper KB and a a query. The restriction ofE wrt a , denoted Ela, is the set {V( e :J l) E E I the predicate of l appears in a}.

Proof: The proof is by induction on the structure of a . Here we only prove the case for quantifications. V[E, 3xa] = max{V[E, ad] I d E H+ (E U {a })} = (by induction) max{V[E Ia, a d] I d E H+ (E U {a})} = (by Corollary 2.4) max{V[Eia, ad] IdE H+(Eia U {a})}= V[Eia, 3xa]. ·

In fact, we can go further than this: roughly speaking, we need only consider those sentences V( e :J l) E E such that after substitutions dictated by e, the l would unify with some literal in the query a . For example, Vxy(y = b :J P(x, y)) is not needed to answer the query 3xP(x, a). For KBs that are large because they have facts about a large number of in­ dividuals, this optimization can reduce significantly the size of the KB fragment needed to answer the query correctly.

2.4 Answers to open queries

Definition 2.7 Let E be a proper KB and a (x ) a formula with free variables. The answer to a wrt E is the set a(E) = {c I V[E,a(c)] = 1}.

However, a(E) may well be infinite. Fortunately, we can find a finite representation for it.

Definition 2.8 Let E be a proper KB and a a formula. Then H(E, a) is the finite set of constants consisting of those men­ tioned in E or a and the r next ones, lexicographically, where r is the quantifier rank ofVa .

Definition 2.9 Let ~ be a proper KB and a(x) a formula with free variables. The finite answer to a wrt ~ is the set a1 (~) = {c E H(~la, a ) IV[~, a (c)] = 1}.

The following theorem justifies a 1 (~) as a finite represen­ tation for a(~).

Theorem 2.10 Let~ be a proper KB and a(x) a formula. Then for any constants c, c E a(~) iffc* E at(~). where c* is like c except that constants not in ~Ia U {a} are replaced by unique representatives not in ~Ia U {a } from H(~la , a ).

Proof: We can expand * to a bijection * from C to C such that c* = c for any c that appears in ~Ia or a. Then V [~, a( c)]= (by locality) V[~la, a(c)] =(by Theorem 2.3) V[(~la)* , (a(c))*], i.e. V[~la, a(c*)] =V[~, a(c *)]. ·

3 The .complexity of database queries

3.1 An overview

The complexity of query evaluation has been one of the main pursuits of database theory. Traditionally, there are two com­ plexity measures: combined complexity and data complexity [Vardi, 1982]. Combined complexity is measured in terms of the combined size of the database and the query. Chan­ dra and Merlin [1977] proved that the combined complexity of conjunctive queries (queries expressed by first-order for­ mulas that are of the form 3x ( a 1 1\ . . . 1\ an) where ai are atoms) is NP-complete; Vardi [1982] proved that the com­ bined complexity of first-order queries is PSPACE-complete. However, the main factor responsible for this high complexity is the size of the query and not the size of the database. This is contrary to the situation in practice where we normally eval­ uate small queries against large databases. Data complexity measures the complexity of query evaluation solely in terms of the size of the database and treats the size of the query as a constant. A folk result is that first-order queries can be evalu­ ated in time n°(l), where n is the size of the database and l is the size of the query. Thus the data complexity of first-order queries is in PTIME. However, such a complexity can hardly qualify as tractable even if the exponent is small, say 5.

Yannakakis [1995] was the first to suggest that parameter­ ized complexity [Downey and Fellows, 1995] might be an appropriate complexity measure for database query evalua­ tion. Query evaluation is fixed-parameter tractable if there is a computable function f : N --... N and a constant c such that the problem can be solved in time f ( l) · n c, where l and n are the size of the query and the database, respectively. However, Papadimitriou and Yannakakis [1999] proved that the param­ eterized complexity of conjunctive queries is W[1]-complete and thus most likely not fixed-parameter tractable. We re­ fer the reader to [ Grohe, 2002] for a survey on parameterized complexity in database theory.

Therefore database query evaluation in general is hard with respect to both combined and parameterized complexity. And yet, database queries do work quite well in practice, even for very large databases. A careful examination of the hard­ ness results show that they often depend on queries that are somewhat atypical in applications, e.g. databases represent­ ing graphs and queries asking for the existence of cliques.

Naturally, many research efforts have gone into finding classes of queries that can be proven tractable, even in the worst cases. The earliest result of this form, due to Yan­ nakakis [1981], showed that acyclic conjunctive queries can be evaluated in polynomial time. This result has been ex­ tended in several ways. The first extension, due to Chekuri and Rajaraman [ 1997], showed that conjunctive queries with bounded treewidth are tractable. Later, Gottlob et al. [ 1999] introduced the notion of hypertree width and showed that conjunctive queries with bounded hypertree width are tractable; bounded hypertree width generalizes the notions of acyclicity and bounded treewidth. Recently, Flum et al. [200 1] generalized the notions of acyclicity and bounded treewidth from conjunctive queries to nonrecursive stratified Datalog (NRSD), which is known to have the same expres­ sive power as all of first-order logic, and showed that acyclic and bounded treewidth NRSD are tractable. Inspired by their work, Gottlob et al. [2001] extended the notion of hypertree width to NRSD, and obtained a nice logical characterization of hypertree width: they showed that the k-guarded fragment of first-order logic has the same expressive power as NRSD ofhypertree width at most k. Thus k-guarded first-order logic turns out to be the largest tractable class of queries so far.

3.2 An evaluation algorithm

The guarded fragment GF was introduced by Andreka et al. [ 1996], and has recently received a lot of attention. The idea is that any existentially quantified subformula ¢ must be con­ joined with a guard, i.e. an atom containing all free variables of¢ . Gottlob et al. [200 1] extended GF to the k-guarded frag­ ment GF k where up to k atoms may jointly act as a guard, and proved that GFk-formu1as can be evaluated in time O(l 2 nk) where l and n are as before. The proof is by transforming GFk-formulas into k-guarded NRSD programs.

In this section, we introduce the k-guarded fragment of .C, and explicitly present a polynomial algorithm for evaluating k-guarded formulas against databases and analyze its com­ plexity. We will use this algorithm to evaluate k-guarded for­ mulas with respect to proper KBs.

Definition 3.1 The k-guarded fragment GFk of .C is the smallest set of formulas such that

1. GFk contains atoms and equalities;
2. GFk is closed under Boolean operations;
3. GFk contains 3x(G1 1\ ... I\ Gm 1\ ¢ ),provided that the Gi are atoms or equalities, m :<:::: k, ¢ E GFk. and the free variables of¢ appear among the Gi.

Definition 3.2 The strictly k-guardedfragment SGF k are the formulas in GFk of the form 3x(G11\ . .. 1\Gm /\¢). We allow the degenerate cases where x is empty or m = 0 or ¢ is TRUE.

Note that any k-guarded sentence is strictly k-guarded.

The evaluation algorithm below will take a strictly k­ guarded formula as the query. It turns out that any formula ¢can be transformed in linear time into an equivalent SGFk­ formula for some k, using guards of the form x = x, if neces­ sary. For example, note that R(x , y, z )l\ S(z , u , v ) can be for­ mulated in SGF2, but ·R(x, y , z )I\·S(z , u , v) only in SGF5.

The evaluation algorithm will have worst-case time com­ plexity that is exponential only in the k. For fixed k, the algo­ rithm is polynomial, but perhaps impractical when k is large. An upper bound on k is the width of¢. Obviously, if ¢ has at most k distinct variables, the width of¢ is no more than k.

Before presenting the evaluation algorithm, we first recall some basic notions of relational database theory. A database instance is simply a logical structure (or interpretation) with a finite domain. Let A be such a structure with domain A. Let X and Y be sets of variables. An X -relation Rover A, is a finite set of mappings 1 from X into A, which we write as {r: [X---> A]}. IfY ~ X, theY-projection of an X-relation R, which we write ny(R), is the set {riY I 1 E R}, where 11Y is the mapping restricted to Y . Let R be an X -relation and S a Y -relation. The join of RandS is the XU Y -relation

• The join of R with the complement of Sis the XU Y -relation R we s = {r: [Xu y ___..A] I IIX E R, IIY (j. S}.

Let ¢ be a formula with free variables X = { x1 , ... , Xn}. The answer to ¢ wrt A is the X -relation

Here is the algorithm for computing answers:

Procedure Eval(A, ¢)

Input: A structure A such that the domain and all relations are sorted, and a formula ¢ E SGF k

Output: <P(A)

suppose ¢(x) = 3y(Gl 1\ ... 1\ Gm 1\ '1/J) returnnx{Eval(A,G1 (A) W ... W Gm(A),'IjJ')} where '1/J' is the result of pushing ·S in 'ljJ so that they are in front of atoms, equalities, or existentials.

Procedure Eval(A, R, ¢) is defined recursively by:

1. If¢ is an atom or an equality, then Eval(A, R, ¢) = R w ¢(A);
2. If¢ is negation of an atom or an equality, then Eval(A, R, ¢) = R W ¢(A);
3. Eval(A, R, (¢ 1\ '1/J)) = Eval(A, R, ¢) n Eval(A, R, '1/J);
4. Eval(A, R, (¢ v '1/J)) = Eval(A, R, ¢) u Eval(A, R, 'ljJ);
5. Eval(A, R, 3y¢) = R w Eval(A, 3y¢);
6. Eval(A, R, ·3y¢) = R W Eval(A, 3y¢).

Theorem 3.3 Given a sorted structure A and a formula¢ E SGFk. ¢(A) can be computed in time O(lnk), where l is the size of¢, and n is the size of the database.

Proof: For each of the l literals and logical operators in the query, we perform either a join, a join with complement, an intersection, or a union. Note that when we perform a join or a join with complement within Eval(A, R, ¢), the attributes of the second argument is always a subset of those of the first, since for guarded formulas, the free variables in¢ are a subset of those in R. By induction, Eval(A, R, ¢) always returns a relation that is a subset of R. Moreover, the R is obtained from joins of at most k guards, and so has size at most n k. Assuming all relations start in sorted form, the results of all operations can be kept in sorted form, and computed in time O(nk). Thus, the time overall is O(lnk). ·

4 The complexity of V

In this section, we consider how hard it is to compute V. Not surprisingly, V is no easier than database query evaluation. What is more significant is that under reasonable assump­ tions, it is not much harder either.

4.1 Intractability results

Theorem 4.1 The combined complexity of V is NP-hard for conjunctive queries, and ?SPACE-hard for first-order queries. The parameterized complexity of Vis W[ I ]-hard for conjunctive queries.

Proof: The proof is essentially the same as that for database query evaluation. For conjunctive queries, the reduction is from the clique problem. For first-order queries, the reduction is from QBF (Quantified Boolean Formula). ·

4.2 A tractability result

We now present a tractability result for V. The basic idea is to reduce V to database query evaluation and use the algorithm Eval from Section 3. To do this efficiently, we would like to use database operations as much as possible, and only reason with the formulas e in V(e :::> l) when necessary. For each predicate P appearing in a query a, we will consider storing two relations p+ and p- depending on the form of I:.

Definition 4.2 The ewff defining a predicate P denoted ep, is the disjunction of all e such that Vx( e(x) :::> P(x)) E I:. The ewff defining -,p denoted e~p is analogous.

Definition 4.3 We distinguish among three cases for an ewff:

1. e is relational if it is of the form x = c1 V ... V x =En where n;::: 0.
2. e is co-relational if it is of the form x -:J c1 1\ ... 1\ x -:J Cn where n > 0.
3. e is unrestricted otherwise.

Definition 4.4 Thee-size of I: is the maximum size of an un­ restricted ep or e~p in I:.

For each predicate P, we store p+ as a sorted relation when ep is relational or co-relational, and analogously for p- us­ ing e~P· We let DB(L:, C) (where C is a set of constants that includes all those in I:) denote the database whose domain is C and whose relations are p+ and p- as above.

Note that in the case of a predicate P in I: corresponding to a normal database-style relation, ep will be relational and e~p will be co-relational and the two relations p+ and p­ will be identical. A simple optimization would merge them.

Next, given a formula a we construct a database query by replacing every occurrence of a predicate Pas follows: a pos­ itive3 occurrence of P is replaced by p+ when e p is rela­ tional, ,p+ when co-relational, and by ep itself otherwise; a negative occurrence of P is replaced by ,p- when e~p is relational, p- when co-relational, and by ·e~p itself oth­ erwise. We let Q(I:, a) denote the resulting database query with double negation removed.

We present examples of this transformation in the next sec­ tion. Here we note the following correctness result:

3 A positive (resp. negative) occurrence of P in a is one within the scope of an even (resp. odd) number of negations.

Theorem 4.5 Let I: be a proper KB and a a formula of .C. Let C = H(L:Ia, a), A = DB(L: Ia, C), and¢> = Q(L: , a). Then at(L:) =¢>(A).

This theorem says that the (finite version of) answers to open queries in .C correspond exactly to the answers we get for the database constructed as above. This is a consequence of locality and the following lemma:

Lemma 4.6 Let I: be a proper KB and a a sentence of .C. Let C be any finite set of constants consisting of those in I: U {a} and k extra ones for some k 2:: qr(a). Let A= DB(L:Ia , C). Then V[L:, a] = 1 iff A f= Q(I: , a), and V[L: , a ] = 0 iff A F= Q(I: , -.a).

Proof: The proof is by induction on the structure of a. Here we choose to prove the case for V[I:, a] = 0 which is trickier than the case for V[I:, a] = 1.

The case fort = t' is trivial. V[I: , -.a] = 0 iff V[I:, a] = 1 iff (by induction) A f= Q(I:, a), i.e. Q(L:, -.-.a) .

Consider a V {3. Let Q(I:,-.a) = -.¢>and Q(I:,-.{3) = -.'lj;. Then Q(I:, -.(a V {3)) = -.(¢> V 'lj;). V[I:, a V {3] = 0 iff V[I: , a] = 0 and V[I:, {3] = 0 iff (by induction) A F= Q(I: , -.a) and A F= Q(I:, -.{3) iff A F= -.¢> A -.'1/J iff A f=-.(¢> V '1/J), i.e. Q(L: , -.(a V {3)).

Consider :Jxa. Let Q(I:,-.a) = -.¢>. Then Q(I:,-.:Jxa) = -.:lx¢>. V[L:, :lxa] = 0 iff V[I:, ad] = 0 for any d E H+ (I: U {a}) iff (by Corollary 2.4 since C contains at least one constant not in I: U {a}) V[L:, ad] = 0 for any d E C iff (by induction since C consists of those constants in I: U {ad} and j extra ones for some j 2:: qr(a)) A f= Q(I:, -.ad), i.e. -.¢>d for any d E C iff A f= 'Vx-.¢> iff A f= -.:lx¢>, i.e. Q(I:,-.:lxa). ·

To obtain a tractability result for open queries over proper KBs, we need only ensure that the database queries we con­ struct are k-guarded then use the Eva! procedure.

Definition 4.7 Let I: be a proper KB. The strictly k-guarded fragment SGk (I:) of .C for I: is the same as SGF k except that when :Jx( G1 1\ ... 1\ Gm 1\ ¢>) is within the scope of an even ( resp. odd) number of -.s, the Gi must be equalities or atoms P(f) s.t. ep is relational (resp. e~p is co-relational) or liter­ als -.P(f) s.t. e~p is relational (resp. ep is co-relational).

Clearly, for any a, if a E SGk(I:), then Q(I:, a) E SGFk. Note that every formula a with width m can be transformed into an equivalent SGk(I:)-formula for some k :::; m, using equalities as guards if necessary.

Now we get our main complexity result:

Theorem 4.8 Let I: be a proper KB and a E SGk(I:). Then a1(L:) can be computed in time O(lwnk), where lis the size of a, n is the size of I: Ia, and w is thee-size of I: Ia.

Proof: Let C = H(L:Ia, a), A = DB(L:Ia, C), and ¢> = Q(L: , a). We sort C. By Theorem 4.5, at(L:) = Eval(A, ¢>).

The size of A is O(n), and the length of ¢> is O(lw) . By Theorem 3.3, a1(L:) can be computed in time O(lwnk). ·

As a special case of the theorem, we have:

Corollary 4.9 Let I: be a proper KB and a a sentence in SGk(L:). Then whether V[L:, a] = 1 can be decided in time O(lwnk), where l, wand n are as above.

Corollary 4.10 Let I: be a proper KB and a E NF n SGk(L:L. Then whether£ U I: f= a can be decided in time O(lwn ). where l, wand n are as above.

Proof: Follows from previous corollary and the fact that V is logically sound and complete for queries in NF. ·

Note that these bounds are identical to their database coun­ terparts modulo the w factor. In most cases of interest, the w will be small since even in a large KB, we only expect to see a large ep or e~p in database-like cases, where the e is relational or co-relational. In the case where none of the e are relational or co-relational, we get the following:

Corollary 4.11 Let I: be a proper KB and a a formula of width k with all literals defined by an unrestricted ewff. Then a1(L:) can be evaluated in time O((lw)k+l), where lis the size of a, and w is the e-size of I: Ia.

Proof: We transform a into an equivalent SGk(I:)-formula, using equalities as guards. The size of I:la is O(lw). ·

5 An example

To illustrate how query evaluation would work with proper KBs, we return to the example robotic scenario mentioned in the first section, involving the predicate In(person, room). We can see from the example that e1n is given in relational form, while e~In is given in unrestricted form. To make things interesting, we assume two more predicates: One is Mgr(person 1 , person 2 ) saying that the first person is a man­ ager and that the second is one of his or her employees; we assume that Mgr is given as a closed database predicate. The other is Cmp(person 1 ,person 2 ) saying that the two persons are compatible. We assume that the robot knows that any two people are compatible except m(> 2) pairs; among these m pairs, the robot only knows that two pairs are not compatible. Hence ecmp is given in co-relational form, and e~cmp is given in relational form. Thus the corresponding database has the following relations: Jn+, Mgr+, Mgr-, Cmp+, and Cmp-, where Mgr+ = Mgr-, and Cmp- ~ Cmp+.

Here are some example queries, with the guards underlined.

1. What rooms are unoccupied?
2. r = r 1\ -.:lx(x = x 1\ r = r 1\ Jn(x, r))
3. Are there rooms with more than one manager in them? :Jdm:lm'(Jn(m,r) 1\/n(m',r) 1\m =f. m' 1\ :lxMgr(m,x) 1\ :Jx'Mgr(m',x'))
4. Are there any managers whose employees are all in the same room?

1. Is it true that any two people who are not compatible are in different rooms?

Observe that in all cases, the queries are strictly 2-guarded wrt the proper KB. Also, because no query contains a lit­ eral and a unifiable literal of opposite polarity, from results in [Levesque, 1998], all the queries are in N:F.

The corresponding database queries are as follows :

1. r = r 1\ ·:lx(x = x 1\ r = r 1\ ·e~tn(x, r))
2. :Jr:Jm:Jm'(In+(m, r) 1\ In+(m', r) 1\ m =I m' 1\ :JxMgr+(m, x) 1\ :Jx' Mgr+(m', x'))
3. :Jm:Jr(m = m 1\ r = r 1\ ·:lx(Mgr- (m, x) 1\ r = r 1\ ·In+(x, r)))
4. -,:Jx:Jx' ( Cmp+ (x, x') 1\

-,:Jr:Jr'(In+(x, r) 1\ In+(x, r') 1\ r =I r'))

6 Conclusions

In this paper, we have shown how a bottom-up query evalua­ tion procedure for databases can be used to answer queries for KBs with a certain form of incomplete knowledge. Although this procedure can be impractical for k-guarded queries where k is large, they would be impractical for databases too.

A number of questions remain to be addressed. First of all, Lakemeyer and Levesque [2002] have proposed an extension to proper KBs that allow disjunctions in the KB. It would be interesting to see how much of the database retrieval mech­ anism could be preserved in this case. We can also imagine other extensions to proper KBs, such as relaxing the unique name assumption over constants, or allowing a limited use of function symbols. Also, as suggested in the first section, we can imagine a dynamic scenario where at any given point what a robot or agent knows about the current situation is ex­ pressible as a proper KB. It would then be useful to amalga­ mate regression-based techniques for reasoning about change from [Reiter, 2001] with the database techniques considered here. Among other things, this would require determining those cases where the successor state axioms guarantee that a proper KB remains proper after an action has been per­ formed, perhaps along the lines of [Petrick and Levesque, 2002]. It would also be interesting to investigate the relation­ ship between proper KBs and other subsets of logic to see if the complexity results presented here can be further gener­ alized. Two immediate candidates are datalog programs and stratified logic programs that include some form of classical negation. Finally, we note that additional optimizations can be made to our query evaluation procedure that do not change the worst-case performance, but would improve its behaviour in practice.

Acknowledgments

We would like to thank Leonid Libkin for pointing us to the relevant database literature. Financial support was gratefully received from the Natural Sciences and Engineering Research Council of Canada.