Efficient Reasoning in Proper Knowledge Bases with Unknown Individuals

1 Introduction

As argued by Levesque [1998], there is to date really only one logically correct deductive reasoning technique that appears to be efficient enough to be feasible for large knowledge bases (KBs) containing (say) millions of facts: database retrieval. (SAT solving does show promise too, but not for deduction and not for first-order reasoning.) Viewed in logical terms, however, a database requires complete information: every atomic formula must be known to be true or known to be false. In particular, databases (typically) make a closedworld assumption: anything not explicitly recorded as true can be assumed to be false. Yet many AI applications must survive in an open-world setting, with incomplete information of their domain, often acquired incrementally over time (e.g. a robot that must sense its environment to determine if there are boxes nearby, or a travel-agent softbot that gathers information about available flights over the web).

Levesque [1998] raises the question: for what sorts of logical theories can we retain the deductive efficiency of database retrieval without requiring complete knowledge? To answer it, he proposes the notion of a proper knowledge base, where incomplete knowledge amounts to a possibly infinite set of positive or negative ground facts. For this kind of KB he devises a reasoning procedure based on formula evaluation, Hector J. Levesque University of Toronto Toronto, Canada hector@cs.toronto.edu which he shows is logically sound and sometimes also complete. Most interestingly, the procedure is essentially as efficient as query evaluation in databases with complete information [Liu and Levesque, 2003; Liu, 2006]. However, one serious limiting element of this proposal is that a proper KB cannot include knowledge about individuals whose identity is unknown.

Incomplete information has also been studied in databases [Imielinski and Lipski, 1984; Reiter, 1986; Vardi, 1986; van der Meyden, 1998], and recently it is acquiring new importance in the context of uncertain databases, connected with probabilistic approaches [Agrawal et al., 2010; Antova et al., 2009], XML semistructured data [Abiteboul et al., 2006; Barcel´o et al., 2010], and most prominently in data integration and data exchange [Lenzerini, 2002; Kolaitis, 2005]. Interestingly, in much of this work, incomplete information comes in the form of unknown individuals (or labeled null values), i.e., we know that there exists an object with certain properties, but we cannot really identify it (though we may still use it in joins, and more generally, in formulas). Incomplete information of this form is tightly linked with the problem of query containment, and more specifically with query containment involving conjunctive queries [Chandra and Merlin, 1977; Ullman, 1997; Lausen and Wei, 2003]. Indeed Chandra and Merlin showed that a conjunctive query can be seen as a database with labeled nulls and conversely, that a database with labeled nulls can be seen as a conjunctive query. This observation has led to a rich theory which is at the base of modern approaches to data integration and data exchange, including the work on ontology-based data access and integration proposed within the AI community [Poggi et al., 2008].

In this paper we combine ideas from these two lines of research. We obtain a generalization of Levesque's proper KBs that handles both missing facts (like the original version) and information about unknown individuals (as in the database literature). In this way, we obtain one of the most expressive open-world settings for which reasoning can still be done by evaluation as in closed-world databases. Specifically we devise a query answering procedure and show that it is always logically sound and is also logically complete when the query is in a certain normal form. We analyze its computational complexity, showing that as long as the number of unknown individuals remains small (logarithmic in the size of the KB), the reasoning can indeed be implemented efficiently.

The rest of the paper is organized as follows. In Section 2, we review databases as knowledge bases with a builtin closed-world assumption, and proper KBs as open-world knowledge bases. In Section 3, we show how to handle unknown individuals (null values) in proper KBs, while retaining the same sort of efficiency and soundness and completeness properties. Finally in Section 4, we draw some conclusion and discuss future work.

2 Proper Knowledge Bases

We use an ordinary first-order logical language L with an infinite supply of predicate symbols (including =), an infinite supply of constants we call standard names (which we write as #1, #2, #3, . . .), and no other function or constant symbols. We use the notation αxn to mean the result of replacing every free occurrence of variable x in formula α by standard name n. In this paper, we will be using the normal Tarski semantics for L, with |= understood as normal logical entailment.

However, we wish to make the unique name assumption for the standard names. What this means is that for any knowledge base KB ⊆ L and any query α ∈ L, instead of asking if KB |= α, we will always be asking if E ∪ KB |= α where E is the usual axioms of equality (reflexitivity, symmetry, transitivity, and substitution of equals for equals) together with

Using E in this way has a number of interesting properties. In particular, it can be shown that whenever the KB is finite (as it will always be here), the set (E ∪KB) has a model iff it has a standard model, that is, one where where = is interpreted as identity and the domain is isomorphic to the set of standard names (see [Levesque, 1998], Theorem 2). So this gives us what amounts to an infinitary version of a domain closure assumption. Another property we will use is this:

Theorem 1: [Levesque, 1998] Suppose that KB is finite and H contains all the standard names that appear in KB or α and at least one other standard name. Then

This means that we can determine whether ∀xα is entailed by checking whether a finite set of instances of α are entailed.

Now let us consider databases under the closed-world assumption. Following Reiter [Reiter, 1986], we can think of a database as a logical theory formed by a finite set of ground atoms A, those explicitly in the database, augmented with a set of negated atoms obtained by applying the closed-world assumption, i.e., we can take the KB to be A ∪ {¬P(⃗n) | ⃗n is a vector of standard names and P(⃗n) /∈ A}. Then for any query α, we can decide if E ∪ KB |= α using the following procedure:

1. V [KB, P(⃗n)] = {1 if P(⃗n) ∈ A 0 otherwise 2. V [KB, (n = n′ )] = {1 if n and n′ are the same standard name 0 otherwise 3. V [KB, ¬α] = 1-V [KB, α]

(We can treat (α ∧ β), (α ⊃ β), (α ≡ β) and ∀xα as abbreviations.) V simply evaluates the truth of α in the model corresponding to E ∪ KB in the obvious way.

Proper KBs generalize databases to support open-world reasoning, where we do not require every formula or its negation to be known [Levesque, 1998]. Specifically a proper knowledge base KB is a finite collection of sentences of L of the form ∀⃗x (e ⊃ ρ), where

• e is an ewff, i.e. a quantifier-free formula whose only predicate is equality, and

and such that E ∪ KB is consistent.

It can be shown that a proper KB is a finite representation for a possibly infinite consistent set of ground literals:

In this paper, θ is a substitution of free variables by standard names, and αθ denotes α after the substitution.

Proper KBs have many interesting properties. Unlike databases, we can leave the status of some literals open.

Also, we can make the closed-world assumption for some of the predicates by including both ∀(e⊃ρ) and ∀(¬e⊃ρ), for some e and ρ.

Example 2: Let KB stand for

This amounts to making the closed-world assumption on P .

Any finite set of ground literals can be reformulated as a proper KB, by simply rewriting any ground literal ρθ in the set as ∀⃗x (⃗x = ⃗xθ ⊃ ρ). Some infinite sets of literals can also be represented, e.g., ∀x, y, z(x ̸= z ∧ y = #3 ⊃ R(x, y, z)).

Reasoning with proper KBs. Although proper KBs are quite restricted, it remains undecidable to determine whether or not E ∪ KB |= α. (Consider the case KB = { }, where we still need to determine whether an arbitrary first order formula is valid.) As an alternative, Levesque [1998] proposes a limited reasoning procedure V [KB, α], based on the evaluation function used for databases under the closed-world assumption, that returns 1 (known to be true), 0 (known to be false), or 12 (unknown), defined as follows:

1. V [KB, (n = n′ )] = {1 if n and n′ are the same standard name 0 otherwise
2. V [KB, ¬α] = 1-V [KB, α]
3. V [KB, (α ∨ β)] = max {V [KB, α], V [KB, β]}
4. V [KB, ∃xα] = maxn∈H V [KB, αxn ]

The procedure V has been shown to have several interesting properties. First of all V is tractable in a very strong sense.

1. If e is a ground ewff, then E |= e iff V [{}, e] = 1 and can be determined in time linear in |e|.
2. V [KB, ρθ] can be determined in time linear in |KB|: scan KB for ∀(e ⊃ ρ) or ∀(e ⊃ ρ) and check if E |= eθ.
3. Overall, computing V [KB, α] can be made as efficient as database retrieval [Liu and Levesque, 2003].

Also V is logically sound:

Theorem 2: [Levesque, 1998]

• If V [KB, α] = 1, then E ∪KB |= α.
• If V [KB, α] = 0, then E ∪KB |= ¬α.

However V is not (and cannot be) logically complete in general. For example:

Completeness for queries in the normal formNF. To get completeness one has to consider suitable sublanguages of L. One interesting sublanguage is NF [Levesque, 1998].

First, let us say that a set of sentences S is logically separable iff for every consistent set of literals L, if L ∪ S has no standard interpretation, then for some α ∈ S, L ∪ {α} has no standard interpretation. Then the normal form NF ⊆ L is defined as the least set such that:

1. If α is a ground atom or ewff, then α ∈ NF.
2. If α ∈ NF then ¬α ∈ NF.
3. If S⊆ NF, Sis logically separable, and S is finite, then ∧S ∈ NF .
4. If S ⊆ NF S is logically separable, and S = {αxn | n is a standard name }, then ∀xα ∈ NF.

V is complete (as well as sound) for queries in NF:

Theorem 3: [Levesque, 1998] For any proper KB and any α ∈ NF we have:

• If E ∪ KB |= α, then V [KB, α] = 1.
• If E ∪ KB |= ¬α, then V [KB, α] = 0.

What sorts of queries can we express in NF? In the propositional case, for any quantifier-free formula α, there is an equivalent formula α′ that is in NF. [Liu and Lakemeyer, 2008] have shown that this does not hold for arbitrary formulas with quantifiers. A counterexample is ∀xy z (R(x, y) ∧ R(y, z) ⊃ R(x, z)). However, some significant classes of L queries belong to NF.

Let's say that two literals are conflict-free iff either they have the same polarity, or they use different predicates, or they use different standard names at some argument position.

Theorem 4: [Levesque, 1998] If all pairs of literals in α are conflict-free, then α ∈ NF.

Notice that this theorem applies for example to conjunctive queries from databases.

3 Dealing with Unknown Individuals

Proper KBs can represent some open-world knowledge, but only for individuals whose identity is known. There is no way for a proper KB to say that something has a certain property, without saying what the standard name of that thing is. In fact, for α ∈ NF we have the following: If E ∪ KB |= ∃xα, then for some standard name n, E ∪ KB |= αxn . This is (in part) what allows the V procedure to work correctly.

In this section, we consider how to deal with open-world knowledge that involves individuals whose identity is not known. We start by extending our first-order logical language L, so that in addition to the standard names, we include a disjoint countably infinite supply of constants called (labeled) null values (which we write a1, a2, . . .). So now there are two distinct types of constants in L. As constants, null values behave exactly like standard names, except that they are not mentioned by name in E and so the unique name assumption does not apply to them. From now on, let us assume that a proper KB is a a set of sentences as defined earlier, but using this richer language L (i.e., the ewffs in its assertions may contain null values). For example, if our KB is

then we know the individual that is P (that is, #3), but we do not know which individual is Q; all we know is that something (which may or may not be #3) has property Q. In this sense, null values behave just like Skolem constants.

Reasoning with null values. Null values in proper KBs pose a problem for reasoning, because, unlike the original proper KBs, they allow certain types of disjunctive knowledge to be expressed. Consider the following examples:

Obviously, the V procedure, which handles V [KB, (α ∨ β)] by taking the maximum of V [KB, α] and V [KB, β], will no longer work. Similar problems arise with existentials.

To see how we can avoid these problems, let us suppose from now on that the KB uses k null values ⃗a = 〈a1, . . . ak〉, and for simplicity, that any null value that appears in a query α also appears in KB. 1 We can in fact eliminate the null values by repeatedly replacing them by standard names:

1 Dropping this assumption would complicate the technical treatment to follow, though all results still hold. In effect, a null value that appears only in a query can be replaced by a quantified variable.

Theorem 5: Let ⃗H be a set of tuples of standard names 〈n1, . . . , nk〉 such that n1 ranges over the standard names in KB and α plus one more, and for each 1 ≤ i < k, ni+1 ranges over the names that ni ranges over plus one more. Then

The proof of this uses Theorem 1, the Deduction Theorem, and the Skolemization Theorem (that a set of sentences containing an existential sentence is satisfiable iff the set with the existential variable replaced by a new constant is satisfiable). Thus, with a caveat to follow, we are indeed able to reduce the evaluation of a query V [KB, α] possibly involving null values to a finite set of query evaluations V [KB⃗a ⃗n , α⃗a ⃗n ] that do not involve any null values. Note however that these involve looking at different instances of the KB.

The caveat is the following. Before we can use V (as previously defined) over KB⃗a ⃗n and α⃗a ⃗n , we must ensure that KB⃗a ⃗n (that is, the KB with its null values ⃗a replaced by the standard names ⃗n) is a proper KB. KB⃗a ⃗n will certainly have the right form, i.e., a finite set of ∀(e ⊃ ρ) not containing null values. However, we must also ensure that E ∪ KB⃗a ⃗n is consistent! (When it is not, E ∪KB⃗a ⃗n would then entail every query.)

Checking whether E ∪ KB⃗a ⃗n is consistent is non-trivial. Indeed, even though E ∪ KB may be consistent, there can still be values of ⃗n for which E ∪ KB⃗a ⃗n is not consistent.

One possible solution is to restrict the original KB so that this discrepancy between the consistency of the original KB and that of the instantiated KBs never occurs. For instance, we could insist that if a null value occurs in a ∀(e ⊃ ρ) in the KB, then the KB must not contain a sentence for ρ.

Here, we focus on a more robust approach: detect when E ∪ KB⃗a ⃗n is inconsistent and make sure that we return 1 for any query in this case. As it turns out, this can be done by using V .

Theorem 6: Suppose KB is in the proper form and contains no null values. Then E ∪ KB is inconsistent iff there is a predicate P in the KB such that

where eTP is the disjunction of all e s.t. ∀(e ⊃ P(⃗x)) ∈ KB, and eFP is the disjunction of all e s.t. ∀(e ⊃ ¬P(⃗x)) ∈ KB.

Using this result, we can immediately define a queryanswering procedure for proper KBs with null values. However, the resulting procedure would not be very good. While the V can be executed efficiently, we would need to go over the entire KB to look for an inconsistency with some predicate P. Part of what made the query procedure presented in [Liu and Levesque, 2003] practical is that it only had to deal with the part of the KB involving predicates mentioned in the query. Furthermore, to use the above theorem, we would need to examine the entire KB after every substitution of null values by standard names from the KB and from the query.

Handling inconsistency offline. To make the queryanswering procedure practical, we now show that it is possible to do all of the inconsistency checking in advance of seeing any queries. Our procedure works as follows:

• We construct a set of tuples ⃗H0 as in Theorem 5, but for the empty query.
• We construct a table T of those tuples from ⃗H0 such that E ∪ KB⃗a ⃗n is inconsistent, applying Theorem 6.

After all this offline work, with the table T in hand, we are ready to handle any query α, as follows:

• We construct a set of tuples ⃗H as in Theorem 5, this time using the given α. (Some standard names may not have been considered in ⃗H0, as α may include new ones.)
• If some ⃗n ∈ ⃗H matches (see below) an element of T, then we return 1. Otherwise, we return V [KB⃗a ⃗n , α⃗a ⃗n ].

A tuple of names 〈n1, . . . , nk〉 matches another 〈n∗1 , . . . , n∗k 〉 iff the following conditions hold:

1. ni = nj iff n∗i = n∗j ;
2. if ni is in KB, then ni = n∗i ;
3. if ni is not in KB then n∗i is not in KB.

We can compute this matching between two vectors of standard names using a unification-like procedure.

To see why such a procedure works, consider that when we constructed the table T , we considered the standard names in the KB and k new ones. But the actual new ones we used are not special in any sense, since the following theorem holds:

Theorem 7: [Levesque, 1998] Suppose that β is a formula with one free variable x, and that n and m are two standard names that do not appear in β. Then E |= βx n iff E |= βxm. Exploiting such a result, we can show the following:

Theorem 8: For any standard names ⃗n, E ∪KB⃗a ⃗n is inconsistent iff there is an ⃗m ∈ T such that ⃗n matches ⃗m.

So in the end, after computing the table T the final reasoning procedure for a proper KB that uses null values ⃗a is as follows: call a vector ⃗n of standard names consistent if it does not match any element of the table T ; then we define:

The fact that E ∪KB is consistent guarantees that this V is well-defined. Indeed, it can be shown to be sound:

Theorem 9: [Soundness] For any proper KB and query α, each of which may contain null values,

• if V [KB, α] = 1, then E ∪KB |= α;
• if V [KB, α] = 0, then E ∪KB |= ¬α.

As before, the new V procedure is only complete for restricted queries. When a query α contains null values ⃗a, we can let α ∈ NF mean that α⃗a ⃗n ∈ NF (as previously defined) for every vector of standard names ⃗n. 2 Then we get the following theorem:

2 Other definitions of NF with null values are possible.

Theorem 10: [Completeness] For any proper KB and query α ∈ NF, each of which may contain null values,

• if E ∪KB |= α, then V [KB, α] = 1;
• if E ∪KB |= ¬α, then V [KB, α] = 0.

Let us now look at some examples.

Example 7: Returning to Example 4, we let the KB be {∀x(x = a ⊃ P(x)), ∀x(x ̸= a ⊃ Q(x)) }. First let the query α be (P(#5) ∨ Q(#5)). (Thus E ∪ KB |= α.) Then V [KB, α] will consider two names, #5 and say #7.

• For n = #5, V [KBan , P(#5)] = 1. So V [KBan , α] = 1.
• For n = #7, V [KBan ,Q(#5)] = 1. So V [KBan , α] = 1.

So we get the value 1, as desired.

Now let the query α be P(#5). (Thus E ∪ KB |̸= α.) Then V [KB, α] will consider two new names, #5 and say #7.

• For n = #5, V [KBan , P(#5)] = 1.
• For n = #7, V [KBan , P(#5)] = 1 2 .

So we get the value 12 , as desired.

Example 8: Returning to Example 3, we let the KB be {∀x(x = a ⊃ P(x)), ∀x(x ̸= #1 ∧ x ̸= #2 ⊃ ¬P(x))}. First, let the query α be (a = #1∨a = #2). (So E∪KB |= α.) Then V [KB, α] will need to consider three names.

• For n = #1 and n = #2, αan will be a trivially true ewff. So V [KBan , αan ] = 1.
• Any other n is inconsistent.

So we get the value 1, as desired.

Next, let the query α be (a = #4). (So E ∪ KB |= ¬α.) Then V [KB, α] will need to consider four names.

• For n = #1 and n = #2, αan will be a trivially false ewff. So V [KBan , αan ] = 0.
• Any other n is inconsistent.

So we get the value 0, as desired.

Finally, let the query α be (a = #1). (Thus E∪KB |̸= α and E ∪ KB |̸= ¬α.) V [KB, α] will again consider three names.

• For n = #1, αan will be a trivially true ewff. So V [KBan , αan ] = 1.
• For n = #2, αan will be a trivially false ewff. So V [KBan , αan ] = 0.
• Any other n is inconsistent.

So we get the value 12 , as desired.

Computational complexity analysis. We conclude this section with a computational complexity analysis of the proposed technique. We denote by KB/α the knowledge base obtained from KB by removing all assertions that do not involve predicates occurring in α. Let's call the width of a formula the maximal number of free variables occurring in its subformulas [Liu and Levesque, 2003].

First observe that computing V (KB, α) in the case of a KB that is a database amounts to the usual top down first-order query evaluation, see e.g., [Vardi, 1995], which can be done in O(|α| · |KB/α|w ) where, w is the width of α. (Notice that no variables appear in the KB in this case.) If KB is a proper KB without null values, then computing V (KB, α) can be done in time bounded by O(|α| · |KB/α|w+1 ), where w is the width of α [Liu, 2006; Liu and Levesque, 2003].

Since our technique works by substituting null values with the standard names occurring in KB, by applying Liu's result, we get that:

Theorem 11: Given the table T, computing V (KB, α) can be done in time O((h + k)k · |α| · |KB/α|w+1 ) where h is the number of standard names in KB, k is the number of null values in KB, w is the width of α. 3

In addition, we have that:

Theorem 12: The table T can be computed in time O((h + k)k · ℓv · |E|) where h is the number of standard names in KB, k is the number of null values appearing in KB, E is the largest formula of the ∃⃗x(eTP ∧ eFP ) in Theorem 6, ℓ is the number of standard names and null values appearing in E, and v is the maximum number of variables occurring in one such formula. 4

Let us now consider the various parameters separately. We call: data complexity the complexity obtained by considering as the only parameter the number of standard names mentioned in the KB and in α; null value complexity the complexity obtained by considering as the only parameter the number of null values in the KB; KB complexity the complexity obtained considering as the only parameter the size of the KB; finally, combined complexity the complexity obtained considering everything as a parameter.

We observe that checking for inconsistency can be done in NP: guess an assignment for the null values, guess predicate P, guess an assignment for existential values in the formula ∃⃗x (eTP ∧ eFP ) in Theorem 6, and evaluate equalities. Exploiting this observation, we ge that:

Theorem 13: Computing V (KB, α) is in:

• LOGSPACE (or better AC0) in data complexity;
• coNP in null value complexity;
• coNP in KB complexity;
• PSPACE in combined complexity.

We notice that the data complexity and the combined complexity are the same as for the evaluation of a first-order query in databases. Also, the above analysis tells us that to be efficient we really need to have a number of null values that is logarithmic in the size of the KB and similarly for the width of the query. The latter is already true for proper KBs without null values, and for databases.

A simple extension. One of the kinds of things we might want to do with null values is to include equality information about their unknown values in the KB itself. For example, consider a KB that contains the following sentences:

3 Notice that, (h+k)k ≤ |KB|k .

4 Notice that, O((h + k)k · ℓv · |E|) ≤ O(|KB|k+v+1 ).

This is clearly disjunctive information, but it can now be handled as part of the KB without causing any additional computational problems:

1. Let e be the conjunction of the equality sentences we want to include in the KB.
2. As we are constructing the inconsistency table T, we evaluate V [{ }, e ⃗a ⃗n ].
3. If the answer is 0, then E |= ¬e ⃗a ⃗n , so we add ⃗n to T.
4. Then we ignore this e when we evaluate V [KB⃗a ⃗n , α⃗a ⃗n ].

Example 9: Let KB be {} ∪ { (a = #1 ∨ a = #2) }. (So the table T might be {〈#3〉}, for example.) Let α be the query (a = #4). Then V [KB, α] needs to consider four names:

• For n = #1 and n = #2, V [KBan , αan ] = 0.
• For n = #4, and n = #6, n is inconsistent.

So we get the value 0, as desired.

Now, let α be (a = #1∨a = #2∨a = #5). V [KB, α] again considers four names:

• For n = #1 and n = #2, V [KBan , αan ] = 1.
• For n = #5, and n = #7, n is inconsistent.

So we get the value 1, as desired.

Finally, let α be (a ̸= #1). This time, V [KB, α] considers three names:

• For n = #1, V [KBan , αan ] = 0.
• For n = #2, V [KBan , αan ] = 1.
• For n = #5, n is inconsistent.

So we get the value 12 , as desired.

4 Conclusion

First-order logic offers the promise of being able to reason with knowledge that is incomplete, as required in many AI applications. But so far, only formalisms that make a closedworld assumption, such as databases, appear to scale well. However, some simple forms of open-world knowledge can also be dealt with effectively: proper knowledge bases. As we have shown here, these techniques can be extended to deal with unknown individuals, provided that there are not too many of them. The same techniques can also deal with equality information about the unknown individuals. Note that we did not consider how to deal efficiently with KB updates in this paper. This is an issue for further study.

A further interesting extension would be to handle unknown individuals whose identity depends that of other individuals, for example, bestFriend(george), that is, handling Skolem functions rather than simply Skolem constants as we have done here. Handling Skolem functions in the general case is perhaps asking for too much: Suppose e uses Skolem functions but no predicate other than equality. It is now undecidable to determine if E |= e. But it would be interesting to know if there are some useful special cases that can be handled. For example, imagine that Skolem functions cannot appear in a query, and a variant of a proper KB where a Skolem function is only allowed to appear in the head ρ: e.g. ∀x y (e ⊃ P(x, f(x, y))). We leave this issue for further investigation.