Nonmonotonic Databases and Epistemic Queries

1 Introduction

The approach to database query evaluation developed by Levesque [1984] and Reiter [1990] treats databases as first order theories, and queries as formulas of the language which includes, in addition to the language of the database, an epistemic modal operator. In this epistemic query language, one can express questions not only about the external world described by the database, but also about the database itself-about what the database knows. For instance, one can ask not only whether John teaches any classes this semester, but also whether there is a known class that John teaches. The first question will be expressed by a for­ mula like 3xTeaches(John,x); the second, by the epis­ temic formula 3x K Teaches( John, x). The difference be­ tween these queries becomes essential when the database c~:mtains ~ncomplete (for instance, disjunctive) information. Reiter [1988] argues that epistemic formulas are appropriate also for expressing integrity constraints.

*This research was supported in part by NSF grant IRI-

89-04611 and by DARPA under Contract N00039-84-C-0211.

On the other hand, epistemic formulas are used in knowledge representation for the purpose of expressing defaults. Autoepistemic logic ([Moore, 1985], [Levesque, 1990]) is the best known epistemic nonmonotonic for­ malism. One of the reasons why autoepistemic logic is important is that general logic pro!frams can be naturally viewed as autoepistemic theories lGelfond, 1987]. This is no longer the case, however, for "extended" logic pro­ grams, which are capable of handling incomplete infor­ mation [Gelfond and Lifschitz, 1990]. In order to express extended rules by formulas, one has to use other epis­ temic nonmonotonic formalisms. The logic of "grounded knowledge," proposed by Lin and Shoham [1990], is one of the possibilities. 1

This paper brings these two directions of research to­ gether. We describe a new version of the Lin/Shoham system, similar in spirit to the Levesque/Reiter theory of epistemic queries. Our formulation is simpler than that of [Lin and Shoham, 1990], and, unlike the latter it is . , not restncted to the propositional case. Using this formalism, we can give meaning to epistemic queries in the context of logic programming; we can ask what a logic program knows. Because our system contains also (some f?rms of) default lo~ic [Reiter, 1980] and circumscrip­ tion [McCarthy, 1986J, we can give meaning to epistemic queries in the context of a default theory or a circum­ scriptive theory as well.

The system of Lin and Shoham, unlike most other epis~emic nonmonotonic formalisms, uses two epis­ temic operators. One of them represents "minimal knowledge" 2 ; the other is closely related to the concepts of "justification" in default logic and of "negation as fail­ ure" in logic programming. The main technical idea of this paper is to identify the former with the epistemic operator K used by Levesque and Reiter.

1 Other modifications of autoepistemic logic that can be used for this purpose were developed in [Marek and

Truszczynski, 1989j, [Siegel, 1990] and [Truszczynski, 1991].

2 The idea of minimal knowledge (or "maximal ignorance") was formalized, in various ways, by several authors, including Konolige (1982], Halpern and Moses (1984], Shoham (1986] and Lin (198~].

We concentrate here entirely on the semantical issues, and leave aside, for the time being, the computational problems of query evaluation in this framework. 3

2 Propositional MKNF: Formulas and Interpretations

The formulas of the propositional logic of minimal knowl­ edge with negation as failure (MKNF) are built from propositional symbols (atoms) using the standard propo­ sitional connectives and two modal operators: K and not. 4 A theory is a set of formulas (axioms).

If a formula or a theory doesn't contain the negation as failure operator not, we call it positive. If it contains neither K nor not, it is objective.

An interpretation is a set of atoms. The set of all interpretations will be denoted by I. Our first goal is to define when a set S C I is a model of a theory T. As a preliminary step, let us consider the case of positive theories.

3 Positive Theories

For an interpretation I and a set of interpretations S, we define when a positive formula F is true in (I, S), as follows. (For simplicity, we assume that all propositional connectives are expressed in terms of the primitives ..., and A.)

1. IfF is an atom, F is true in (I, S) iff F E I.

2 . ...,p is true in (I, S) iff F is not true in (I, S).

3. FAG is true in (I, S) iff F and G are both true in (I,S).

4. KF is true in (I, S) iff, for every J E S, F is true in (J, S).

A model of a positive theory T is any maximal set S C I such that, for every I E S, the axioms ofT are true in (I,S).

The maximality condition expresses the idea of "mini­ mal knowledge": The larger the set of "possible worlds" is, the fewer facts are known.

In the special case when T is objective, the require­ ment that all axioms ofT be true in (I, S) means simply that I is a model of T in the sense of classical proposi­ tional logic. Consequently, the set Mod(T) of the "clas­ sical models" of T is the only model of T in the sense of MKNF.

As another example, consider the case when T is {KF}, where F is an objective formula. The models of T are the maximal sets S C I such that every inter­ pretation from S is a classical model of F. It is clear that Mod( F) is the only such set. More generally, ifF is an objective formula and To a set of objective formulas, then To U {KF} has a unique model; it is the same as the model of To U { F}, that is, M od(To U { F}).

If T = {KF1 V KF2}, where F1, F2 are objective, then the models of T are the maximal sets S C I that satisfy the condition: Every interpretation from S is a classical model of F1 or every interpretation from S is a classical model of F2; symbolically:

3 An algorithm for the evaluation of epistemic queries in the monotonic case is proposed in [Reiter, 1990].

4 The "assumption operator" A from [Lin and Shoham, 1990]) corresponds, in our notation, to the combination ...,not.

If neither F1 nor F2 is a logical consequence of the other, then neither of the sets Mod(F!), Mod(F2 ) contains the other, and T has two models: Mod(F!) and Mod(F2) .

4 Propositional MKNF: Models

How can we extend the definition of a model to the gen­ eral case, when the axioms contain not?

In the presence of both K and not, truth will be de­ fined relative to a triple (I, S"', S"), where S"' and S" are sets of interpretations; S"' serves as the set of possi­ ble worlds for the purpose of defining the meaning of K, and S" plays the same role for the operator not. Then a model will be defined as any set sn that satisfies a certain fixpoint condition.

For an interpretation I and two sets of interpretations S"', S", we define when a formula is F true in (I, S"', S") , as follows.

1. IfF is an atom, F is true in (I, S"', S") iff FE I.

2. ...,p is true in (I, S"', S") iff F is not true in (I, S"', S").

3. FAG is true in (I, S"', S") iff F and G are both true in (I, S", S").

4. KF is true in (I, S"', S") iff, for every J E S"', F is true in (J, S"', S").

5. not F is true in (I, S", S") iff, for some J E S", F is not true in (J, S", S").

The truth condition for not F expresses that F is not known to be true provided that sn is the set of worlds that are considered "possible."

This definition is a generalization of the definition of truth for positive formulas given in the previous section, in the sense that a positive formula is true in (I, S", S") iff it is true in (I, S").

For any theory T and any setS c I, by r(T, S) we denote the set of all maximal sets S' C I which satisfy the condition:

For every I E S', the axioms of T are true in (I, S', S). (1)

If S E r(T, S), then we say that S is a model ofT.

It is easy to see that, for positive theories, this is equiv­ alent to the definition given earlier. Indeed, if T is pos­ itive, then r(T, S) does not depend on S, and is simply the set of all models of T in the sense defined in the previous section.

As an example of a theory whose axioms are not pos­ itive, consider the theory T whose only axiom is

where F and G are objective. The condition (1) says in this case:

This is equivalent to:

or

Consequently f(T, S) is {I} if S c Mod( F), and {Mod( G)} otherwise. We conclude that the models of (2) can be characterized as follows:

1. IfF is a tautology, then I is the only model of (2).

2. IfF is a not a tautology but is a logical consequence of G, then (2) has no models. For instance, not F :::> F has no models.

3. IfF is a not a logical consequence of G, then the only model of (2) is Mod( G). For instance, not p :::> q, where p and q are distinct atoms, has one model, Mod(q).

5 Relation to Logic Programming

In this section we show that logic programs of some kinds can be viewed as theories in the sense of MKNF. We will consider three classes of programs, moving gradu­ ally towards greater generality. In the semantics of logic programming, it is customary to view a rule with vari­ ables as shorthand for the set of its ground instances; for this reason, we can restrict our attention to propositional programs.

A positive logic program is a set of rules of the form

where m ~ 0, and each Ai is an atom. According to van Emden and Kowalski (1976], the semantics of a positive program IT is defined by the smallest set of atoms which is closed under its rules (that is to say, which includes Ao whenever it includes A1, ... , Am, for every rule (3) from IT) . This set of atoms is known as the "minimal model" of IT, and we will denote it by MM(IT).

In order to relate the semantics of positive programs to MKNF, let us agree to identify a rule (3) with the formula

For any interpretation J, let w( J) be the set of all inter­ pretations I such that J C I.

Theorem 1, Part A. Every positive program IT has one model, w(MM(IT)).

For instance, let the rules of IT be

Then MM(IT) is {r,s}. Viewed as a theory in the sense of MKNF, IT is the set of 3 axioms:

its model w(MM(IT)) is

A general logic program is a set of rules of the form

where n ~ m ~ 0, and each Ai is an atom. Several approaches to defining a semantics for general logic pro­ grams have been proposed. One of them is based on the

If, for some J E S, F is false in J, then, for every I E S', G is true in I, notion of a "stable model" [Gelfond and Lifschitz, 1988]. A stable model of IT is an interpretation satisfying some fixpoint condition. We will denote the set of such inter­ pretations by SM(IT). It is clear from the definition of a stable model that, in the special case when IT is positive, SM(IT) = {MM(IT)}.

A rule (6) will be identified with the formula

Theorem 1, Part B. The set of models of a general program IT is

For instance, the program with the rules

has one stable model, {q}. These rules can be written as

The only model of these axioms is

Finally, we will consider the class of (extended) dis­ junctive databases in the sense of [Gelfond and Lifschitz, 1991], in which classical negation and a form of disjunc­ tion are allowed. A disjunctive database is a set of rules of the form

where n ~ m ~ 1 ~ 0, and each Li is a literal (an atom possibly preceded by -.). The semantics of disjunctive databases defines when a set of literals is an "answer set" of a given database. We will denote the set of answer sets of a disjunctive database IT by AS(IT). If IT is a general logic program, then AS(II) = SM(II).

A rule (7) will be identified with the formula

In order to extend Theorem 1 to disjunctive databases, we need to generalize the definition of the operator w. So far, w(M) is defined when M is an interpretation, that is, a set of atoms. Now M is allowed to be a set of literals. For any set of literals M, M+ is the set of atoms that belong to M, and M- the set of atoms whose negations belong to M; w( M) stands for the set of interpretations I such that M+ C I and M- n I = 0.

Theorem 1, Part C. The set of models of a disjunctive database II is

For instance, the disjunctive database whose only rule lS

has two answer sets: {p} and { -.q}. This rule is the same as the formula

the models of this axiom are

and

6 Propositional MKNF: The Consequence Relation

We say that a positive formula F is a theorem of a theory T, or a consequence of its axioms (symbolically, T I= F), if, for every modelS ofT and every interpretation IE S, F is true in (I, S). Thus theoremhood is defined for positive formulas only. (We do not see any reasonable way to define theoremhood for formulas containing not.)

To illustrate this definition, consider first the special case when all axioms ofT are objective. IfF is objective also, then T I= F if and only ifF is a consequence ofT in the sense of classical propositional logic. If F is allowed to contain K, then the definition of I= turns into (the propositional case of) the definition of ~ from [Reiter, 1990].

If, for instance, the only axiom of T is p V q, then -,Kp is a theorem. If -,q is added as another axiom, this theorem will be lost. Thus the consequence relation I= is nonmonotonic even for objective T .

If II is a general logic program or a disjunctive database, we can ask whether a positive formula F is a consequence of II. For instance, q :> pis not a conse­ quence of the program ( 4), because it is false in one of the interpretations from (5) . Theorem 1 (Part C) shows that a literal is a consequence of II if and only if it be­ longs to all answer sets of II .

We conclude this section with two remarks about gen­ eral properties of the consequence relation. First, we would like to say that every axiom is a theorem, but this makes sense for positive axioms only. It is easy to check, however, that the result of replacing all occurences of not by -,Kin an axiom is a theorem. Second, let F1 and F2 be positive formulas; if KF1 :> KF2 is provable in S5, and T I= F1, then T I= F2. In this sense, the set of theorems is closed under 85.

7 Quantification

Our next goal is to extend the definitions given above to languages with quantification. For simplicity, we con­ sider first-order quantifiers only; extension to the higher­ order case is straightforward.

Consider the language obtained from a first-order lan­ guage C by adding the modal operators K and not. A theory is now a set of sentences of this language; an in­ terpretation is a structure for C. The universe of an in­ terpretation I will be denoted by III. For any nonempty set U, by Iu we denote the set of all interpretations with the universe U.

Let I be an interpretation, and let S"', sn be subsets of I111· Vfe will define when a sentence is true in (I, S"', sn) . To th1s end, we need to extend the language by object constants representing all elements of III; these constants will be called names. Truth will be defined for all sen­ tences of the extended language. We assume that all propositional connectives and quantifiers are expressed in terms of-,, 1\ and V.

1. IfF is an atomic sentence, F is true in (I, S"', sn) iff F is true in I.

2. ..,p is true in (I, S"', sn) iff F is not true in (I, S"', sn).

3. F 1\ G is true in (I, S", sn) iff F and G are both true in (I, S"', sn).

4. VxF(x) is true in (I, S"', sn) iff, for every name e, F(e) is true in (I,S"',sn).

5. KF is true in (I, S"', Sn) iff, for every J E S", F is true in (J, S"', sn).

. 6. notF is true in (I, S"', sn) iff, for some J E sn, F IS not true in (J, S"', sn).

For any theory T, nonempty set U, and subset S of Iu, by fu(T, S) we denote the set of all maximal sets S' C Iu which satisfy the condition:

For every I E S', the axioms of T are true iri (I, S', S) .

If S E fu(T, S), then we say that (U, S) is a model ofT. If all axioms ofT are objective, then the models ofT are the pairs (U, Modu(T)), where Modu(T) stands for the set of classical models of T with the universe U.

With quantification available, we can represent logic programs as axiom sets in a more direct way, without first replacing rules by their ground instances. A dis­ junctive database can be identified with the axiom set consisting of (i) the universal closures of the formulas (8) corresponding to its rules (7), and (ii) appropriate equality axioms (see [Clark, 1978]). This semantics dif­ fers from the one presented in Section 5 in that it permits "non-Herbrand models." 5

A positive sentence F is a theorem of a theory T if, for every model (U, S) ofT and every interpretation IE S, F is true in (I, S). The two properties of the propo­ sitional consequence relation stated at the end of the previous section apply to the first-order case also.

8 Relation to Default Logic and Circumscription

In accordance with the idea of Lin and Shoham [1990], we identify a default

with (the universal closure of) the formula

The following theorem refers to "default logic with a fixed universe" -a modification of the system of [Re­ iter, 1980] proposed in [Lifschitz, 1990]. The main differ­ ence is that, in the standard default logic, parameters of an open default are treated as metavariables for ground terms, whereas the modified system handles parameters as genuine object variables.

Theorem 2. An objective sentence F is a fixed-universe consequence of ( D, W) iff D U W I= F.

This theorem shows that the translation (11) embeds default logic with a fixed universe into MKNF.

In [Lifschitz, 1990] we showed how to embed circum­ scription (with all nonlogical constants varied) into de­ fault logic with a fixed universe. The composition of these two transformations reduces the circumscription of Pin a sentence F(P) to the formula

5 See [Przymusinski, 1989] on the role of non-Herbrand models in logic programming.

The objective consequences of this formula in the sense of MKNF are exactly the sentences that follow from the circumscription in classical logic.

9 Conclusion

The logic of minimal knowledge with negation as failure provides a unified framework for several nonmonotonic formalisms and for the Levesque/Reiter theory of epis­ temic queries. Its semantics, like the semantics of cir­ cumscription and of default logic with a fixed universe, is a generalization of the standard concept of a model of a first order theory; we consider this an important advantage.

However, this unification is not entirely satisfactory, for two reasons. First, the logic of minimal knowledge (even in the propositional case and without negation as failur~ has the following puzzling and unintuitive property. When a theory T is extended by an "explicit definition" of an atom p--by an axiom p :::: F , where p occurs neither in the axioms ofT nor in F-this may af­ fect the class of theorems that do not contain p. In other words, in the logic of minimal knowledge, a "definitional" extension is not necessarily "conservative." This obser­ vation seems to point to a serious defect of the idea of minimal knowledge. Second, MKNF does not cover the important concept of "strong introspection," introduced recently by Gelfond (1991].

Acknowledgments

I would like to thank Michael Gelfond, Katsumi Inoue, Hector Levesque, Fangzhen Lin, Ray Reiter, Grigorii Schwarz and Miroslaw Truszczynski for useful discus­ sions on the subject of this paper.