Programming in Autoepistemic Logic

1 Introduction

There are two serious limitations of traditional logic pro­ grammmg:

1. Negative information is represented indirectly through the absence of positive data, which may be undesirable in situations where a direct repre­ sentation is called for. For example, given a rule fly(x) <--- bird(x) and a fact bird(tweety), we shall be able to infer fly(tweety). However, not every bird can fly. Suppose we know -,jly(tweety), how can we add this fact to the database and keep it consistent?
2. There is no direct way to deal with incomplete infor­ mation. The following example from [Gelfond and Lifschitz, 1990] illustrates this:

Eligible(x) <--- HighGPA(x);

Eligible( ;e) <--- Minority(x), FairGP A(x);

-,£[igible(x) <--- ...,FairGPA(x);

Interview( ;e) <--- notEligible( ;e), nobEligible( ;e).

The first rule says that students with high GPA are eligible for a scholarship; the second rule says a stu­ dent is eligible if he is a minority and has fair GPA; the third rule says that a student with GPA lower than fairness is not eligible; the fourth rule says that students whose eligibility is not determined by the above rules should be interviewed by the scholarship committee. Obviously, not l in the above example represents that l is not known, which is different from the negation of l.

In this paper, we present a framework for programming in autoepistemic logic that incorporates unknown infor­ mation and explicit definition of negative information. We show that for certain programs, consistency is guar­ anteed and the fixpoint and declarative semantics coin­ cide. There are two major differences between this paper and [Gelfond and Lifschitz, 1990]:

1. We provide a syntactic restriction to guarantee the consistency of a program.
2. Our base language is first-order, and we provide a resolution procedure to compute the answer set for restricted programs.

The structure of the paper is as follows: Section 2 gives a brief introduction to autoepistemic logic, its syntax, semantics, variations, and extensions. Section 3 intro­ duces autoepistemic programs. Sufficient conditions are given for the existence of a unique, consistent iterative expansion. A resolution procedure, SLSAE-resolution, is defined in Section 4. Section 5 presents conclusion and future work.

2 Autoepistemic Logic

Autoepistemic logic is defined by Moore [Moore, 1985]. Later Konolige [Konolige, 1988] gave another definition of expansions in autoepistemic logic and showed that it is equivalent to Moore's. The language of autoepis­ temic logic, call it £, is constructed out of a base sublan­ guage £o (e.g. propositional or first order), augmented with a modal operator K. Every sentence in £ 0 is a sen­ tence in £, if ¢ is a sentence in £, then so is K¢. If ¢, 1/J are sentences in £, then so are ...,¢, ¢ 1\ '1/J, ¢ V 1/J, ¢ -+ 1/J. Note that autoepistemic logic itself is proposi­ tional. A sentence has K-rank n if its modal operators are nested to a depth of n. Formally, objective formulas, i.e., formulas in £ 0 , have K-rank 0, K-rank(...,¢) = K­ rank(¢), K-rank(¢ 1\ '1/J) = max(K-rank(¢), K-rank('I/J)), K-rank(¢ V 1/J) = max(K-rank(¢), K-rank('I/J)), and K­ rank(K¢) = K-rank(¢)+1. For example, K(A 1\ KA) has K-rank 2. We use Ln to denote the set of all sentences of K-rank n or less. A theory is a set of sentences. We will use a subscript to indicate a subset of sentences based on the K-rank. For example, if Tis a theory, Tn = T n Ln . We call To the objective part ofT.

In the following discussion, let f= denote the usual entailment relation for classic logic, and Cn be the cor­ responding consequence operator. Semantically, an au­ toepistemic interpretation is a pair < I, T >, where I is an interpretation for £ 0 1 and T is a set of formulas . Satisfaction by an autoepistemic interpretation < I, T > is defined as follows:

1. For every objective sentence </>, FI,T </> iff I f= </>.
2. For every </> E £, F=r ,T K¢ iff</> E T.
3. Satisfaction of compound sentences in £ is defined as usual, i.e., by structural induction.

Let F be a set offormulas, we define F FI,T </>iff f=r T F implies FI,T </>; also define F FT </> iff F FI,T </> fdr all interpretations I .

Now, let SF = { </> : F FT </>}. If F is a set of initial as­ sumptions and Tis a set of sentences possessed by a fully introspective reasoner as knowledge, then Sp should co­ incide with T. This argument is originally from [Moore, 1985], and is further explained in [Konolige, 1988; Marek artd Truszczynski, 1988]. We will call F the base set of knowledge possessed by the reasoner.

Definition 1 An expansion of a base set F is a set T satisfying the following equation:

A base set F may have no expansions and even if it has an expansion, the expansion may not be unique. How­ ever, if there is a unique expansion T for a given base set F, then F FT </> can be written as F f= </> without ambiguity. When both F and </> are objective formulas, this notion of implication coincides with the classic one.

2.1 Strong Autoepistemic Logic

Unfortunately, expansions may not be "well grounded" in the initial set of axioms. For example, the axiom {K</> -+ </> }, has an expansion { </>, K</>, ... }. The reason the spurious sentence </> is in this expansion is because in the very beginning we may assume that it is, hence K¢ is true, and </> can be derived. Clearly such an expan­ sion is not the intended one. Marek and Truszczynski [Marek and Truszczynski, 1989] introduced a variant of the notion of expansion. Their approach requires that a formula </> must be first derived if it is used to prove K¢. They defined an operator A such that:

Let us further define

1 If the base language £o is propositional, then I is simply a truth assignment.

and

Then, T is an iterative expansion [Marek and Truszczyn­ ski, 1989] ofF if

Note that AT (F) is exactly the set of all consequences ofF U { -.K<f> : </> (/. T} in the logic N that uses modus ponens and necessitation (from </> infer K</>) as inference rules. That is,

Marek and Truszczynski called the nonmonotonic logic based on the above logic N strong autoepistemic logic. Every iterative expansion is an expansion [Marek and Truszczynski, 1989], but not vice versa. For example: {Kp -+ p} has an expansion t:(p) that is not iterative: adding formulas ---.K<f> for</> not in t:(p) does not help to derive p.

2.2 An Extension

Autoepistemic logic introduced above is propositional. Limited extensions to first order logic were studied in [Konolige, 1989; Marek, 1989]. Marek [Marek, 1989] for­ mulated the first order stability conditions for a set of formulas T as follows:

1. Tis closed under first order provability.
2. If</> E T, then K</> E T .
3. If</>(/. T, then ·K</> E T.
4. Vz</> E T <=> For all a E D, </>(a) E T, where D is a fixed domain and a is the name of object a.
5. 3z</> E T <=>There exists a ED such that </>(a) E T.

Theories satisfying conditions 1-5 are called stable. A nice result was obtained in [Marek, 1989] for stable the­ ories: If T is stable, then T allows the commutativity of quantifiers and operator K. However, the stability condition is too strong. Usually, we expect 3s K</>( z) =? K3z<f>( z) to be true, i.e., if there is some c such that we know <f>(c), then we should know that 3z</>(z). The converse of this implication needs not hold, i.e., we may know that there is an z such that </>( z) is true without knowing exactly which constant z represents.

In this paper we will assume that every element in the domain has a name. This means that the Bar­ can formula (Vz(Kp(z)) -+ K(Vzp(z))) and its converse (K(Vzp(z)) -+ Vz(Kp(z))) hold. This restriction raises the "universal query problem [Przymusinski, 1989b]." That is, if the program P contains a single clause p( a) then Vzp(z) is true. We adopt the solution suggested in [Gelder et al., 1988; Ross, 1989a] and assume that there is an extra symbol, $, which is never used in the pro­ gram. The symbol $ is regarded as a "generic name" for those elements in the domain that have no representa­ tion in the language alphabet. In other words, Vzp( z) is not true unless it is stated in the program explicitly.

3 Definite Autoepistemic Programs

In this section we define definite autoepistemic programs. The syntax is introduced in section 3.1. Two syntactic constraints, namely, stratification and conservativeness, are formally defined. Section 3.2 presents the fixpoint semantics for stratified and conservative programs. It is shown that the fixpoint has a one-to-one correspondence relationship to the unique iterative expansion of such programs.

3.1 Syntax

A definite autoepistemic program P is a set of rules of the form:

where (1) lis a nonequality objective literal, and (2) each Li, 1 ~ i ~ n, is a literal of the form Kz' or --,Kz', where z' is an objective literal. For simplicity we also assume the following Clark's Equational Theory [Kunen, 1987]: 2

1. X #- Y <--- ·K(X = Y).

The definition of l is the collection of all rules in P with lin the head. Given an objective literal[, we say that l occurs positively (resp., negatively) in P if Kl (resp., · Kl) appears in a rule body in P . Similar to classic logic programs, we define stratification as follows:

Definition 2 A program P is stratified if there is a par­ tition of the program P = P1 U ... U Pn, such that the following conditions hold:

1. If l occurs positively in Pi, then its definition is con­ tained in U;<i P;.
2. If l occurs negatively in Pi, then its definition ts contained in U; <i P; . D

Example 1 Let P be the following program: fly(X) <--- Kbird(X), ·K·fly(X); ·fly(X) <--- Kpenguin(X); bird(X) <--- Kpenguin(X); penguin(tweety). Then P is stratified by: P1 = {penguin(tweety); ·fly(X) <--- Kpenguin(X)}, Pz = {bird(X) <--- Kpenguin(X); fly(X) <--- Kbird(X) , ·K·fly(X)}. D

2 A complete equational theory is a theory for equality where for any two ground terms s and t, either s = t or s ::/= t . In Section 4 we will show that a complete equational theory is necessary for the resolution procedure.

In the definition of stratification we treat positive and negative literals in a symmetric way, which raises the question of consistency. To guarantee consistency, we need additional constraints.

Definition 3 (Conservativeness) A rule with a literall in the head is positively-conservative (resp., negatively­ conservative) if l is a positive (resp., negative) lit­ eral and ·K·l is in the rule body. A predicate p is positively-conservative ( resp., negatively-conservative) if every rule in the definition of p (resp., ·p) is positively-conservative (resp., negatively-conservative). A program Pis positively-conservative (resp., negatively­ conservative) if every predicate in P is positively­ conservative (resp., negatively-conservative). · P is con­ servative if for every predicate p E P, p is either positively-conservative or negatively-conservative. D

For instance, in Example 1, fly is positively­ conservative, bird is negatively-conservative, 3 etc; the program itself is thus conservative. The term "conserva­ tive" indicates a cautious attitude to inferring the head literals. For example, fly is positively-conservative be­ cause before inferring that :e can fly, we always check first that ·fly( :e) is not known. On the other hand, we don't check anything before concluding that something cannot fly.

We say that 11 refers to 12 positively (resp., negatively) if l1 is in a rule head and Kl2 (resp., ·Kl2 ) is in the rule body. For example, p refers to q positively, and to r negatively in {p <--- Kq, ·Kr }.

Definition 4 A dependency graph of a program P is a directed graph representing the "refers to" relation be­ tween literals. An edge (h, 12 ) in the graph is positive if h refers to 12 positively in some rule. An edge ( h, 12 ) in the graph is negative if l1 refers to 12 negatively. D

Lemma 1 P is stratified iff its dependency graph has no cycle containing an negative edge. D

Lemma 2 A stratified program P is conservative iff for each positive literal l in the dependency graph, either (l, ·l) or (·l, l) is a negative edge, but not both. D

3.2 Fixpoint Semantics for Definite Autoepistemic Programs

In this section we present the fixpoint semantics for strat­ ified and conservative programs. We first show that for each stratified program, there exists a mapping induced by the program. This gives a fixpoint characterization of such programs. Then we show that fixpoints are con­ sistent for conservative programs.

Let Up= HpU(··Hp)UEU(··E), where Hp is the Herbrand base of program P, E = {s = t : s and t are ground terms } and --, · S = {·A : A E S} for any set of literals S. In the following I will denote a set of ground literals (including equality literals). I is consistent if In--, · I= 0.

For each program P define Tp as follows:

3 There is no definition for -.bird, so the condition is vac­ uously true.

and Vj, 1 S j S n, l~ rJ. I. } Consider a program P stratified by

and define

In is also denoted by iter(T1, . . . , Tn, 0) to stress the fact that In is computed using Tp, 's in an iterative fash­ ion. We have the following fixpoint characterization of a stratified program P, which is proved similarly to the fixed point theory by Apt, Blair, and Walker [Apt et al., 1988]:

Theorem 1 Suppose Pis stratified by P = (P1 U ... U Pn)· Then

Next we show that stratified and conservative programs preserve consistency.

Theorem 2 Let P be conservative and stratified by P = (P1 u .. . u Pn)· Then I = iter(P1, P2, .. . , Pn, 0) is consistent. 0

Finally, we establish a main result of this paper:

Theorem 3 Suppose Pis conservative and stratified by P = (P1 u ... u Pn)· Let I =

iter(P1, P2, .. . , Pn, 0). Then T = e(I) is the unique iterative expansion of P.

(Here £ is the operator of [Marek, 1989] defined in Sec­ tion 2) 0

Theorem 3 shows that the construction of the fixpoint I for a program P is independent of any particular strati­ fication of P.

4 SLSAE-resolution

In this section we define SLSAE-resolution (SLS­ resolution for AutoEpistemic programs) for stratified and conservative programs. SLSAE-resolution is simi­ lar to SLSC-resolution defined in [Przymusinski, 1989a], but is designed for autoepistemic programs. In autoepis­ temic logic, the deduction rule does not hold, i.e., "from ¢infer K¢" does not make(¢-+ K¢) a theorem. We will use ¢ f- 1/J to denote the inference rule "from ¢ infer 1/J."

Definition 5 An inference rule ¢ f- 1/; is sound with respect to a set of axioms p if for all substitutions 8, P F=s \/¢8 implies P F=s \/1/;8 for all iterative expansions S of P. Here V quantifies over all unbounded variables in the formula. 0

Lemma 3 An inference rule¢ f- 1/J is sound with respect to p iff for all ground substitutions 8, p F=s ¢8 implies P F=s 1/;8 for all iterative expansions S of P . o

Definition 6 A formula ¢ is complete with respect to P if for every ground instance ¢' of¢, either P F=s ¢' or P F=s -.¢' for all iterative expansions S of P. 0

For example, introspective formulas (i .e., formulas of the form K¢, where ¢is any formula) and equality formulas are complete formulas with respect to any program P.

Lemma 4 Let ¢ be a complete formula with respect to P with free variable z, then K:3z¢(z) f- :3:eK¢(:e) is sound. (Note that, as described in Section 2.2, ::Jx K¢( ;e) f- K::J:e¢( ;e) is sound for any formula ¢.) 0

Lemma 5 Let ¢ be a complete formula with respect to P. If¢ f- 1/; is sound then -.1/J f--.¢ is sound. 0

Note that the converse of Lemma 5 does not hold. For example, suppose p is the only predicate symbol and a, b, c are the only constants. Consider P = {p(a), -.p(c)}. Here p(:e) f- :e = a V z = b and :e f:- -.a 1\ ;e f:- -.b f- -.p( z) are sound, but p( :e) is not a complete formula.

Similar to classic logic programming, we define goal, query, and answers to a query. The definitions are with respect to a stratified and conservative program P.

Definition 7 A goal G is a headless clause <-­ £1, . .. , L~c, where k 2: 0 and each Li is a literal. We also write G =<-- Q, where Q = Lll .. . , L~c, and refer to either G or Q as a query. 0

Definition 8 An equality literal is (i) an equality (t1 = t 2) or (ii) an inequality 'v'(t1 f:- t2), where V quantifies some (perhaps none) of the variables occurring in the equality literal and t1 and t 2 are terms. A simple equality formula is of the form

where the li 's are equality literals and :3 quantifies over some (perhaps none) of the variables occurring in the li 's. A normal equality formula is of the form

where each Si, 1 :::; j :::; m, is a simple equality formula. 0

The following theorem is from [Chan, 1988; Przymusin­ ski, 1989a], adapted to autoepistemic logic:

Theorem 4 For every equality formula E with n free variables :ell . . . , Zn, there exists a normal equality for­ mula N E such that both F f- N F and N F f- F are sound with respect to Clark's Equational theory. 0

Definition 9 A simple equality formula A is an answer to a query <-- Q if A f- Q is sound. 0

Definition 10 A query Q is solvable if there is a finite set S = {A1, .. . , An} of SLSAE-answers to Q, as de­ fined in the SLSAE-resolution below, such that for any SLSAE-answer A to Q, A f- A1 V .. . V An is sound. {A1, ... , An} is called a complete-answer-set to Q. A program P is solvable if every query Q to P is solvable. 0

In the following, we will assume that the program is solvable. SLSAE-resolution is sound and complete for solvable programs. In particular, if { A1 , . .. , An} is a complete-answer-set to Q, then A1 V . . . VAn f- Q is sound. By Theorem 5 below, Q f- A1 V ... VAn is sound. Since both Q and A1 V ... VAn are complete formulas , by Lemma 5 we have that both -.(At V ... VAn) f- -.Q and ·Q f- -.(At V ... VAn) are sound. Then, by Theorem 4, there is a normal equality formula Bt V ... V Bm equivalent to ·(At V ... VAn), so that {Bt, ... , Bm} is a complete­ answer-set to -.Q.

Suppose {Pt, ... , Pn} is a stratification of P. For any literal L, let stratum( L) = i if L = Kl and i is the unique integer such that the definition of l belongs to Pi. If L = -.Kl and i is the unique integer such that the definition of l belongs to Pi, then define stratum(L) = i+ 1. Note that stratum(Kl) = 1 if lis an equality literal and stratum( Kl) = 2 if l is an inequality literal. Also assume that -.KV(tt #- t2) is simplified to K(tt = t2) by the equational theory.

Let G be a goal <--- Lt, . .. , L1c. We define stratum( G) as follows:

stratum( G) =

We will also write stratum( Q) instead of stratum( G) for G =<--- Q.

Definition 11 Suppose that 8 is some substitution for free variables in V(tt #- t2). The inequality V(tt #- t2)8 is valid if it 8 and t28 cannot be unified. It is satisfiable if ttB and t 28 cannot be unified by binding only universally quantified variables. 0

If an inequality is unsatisfiable, it can not be in any an­ swer. If an inequality is valid, it does not contribute to the information in an answer. Only satisfiable, but non-valid inequalities will appear in an answer, they are called primitive inequalities [Chan, 1988]. We define SLSAE-resolution as follows:

Definition 12 (SLSAE-resolution) Let P be a strati­ fied, conservative, and solvable program, R any fixed computation rule that selects exactly one literal from a given goal at a time. The only restriction is that R never selects primitive inequalities relative to the current sub­ stitution. Let G be any goal with variables :z:t, ... , :Z:n· By induction on the stratum of G, define:

1. SLSAE-tree T( G) for G, each node ofT( G) is la­ beled with a goal;
2. Success leaves ofT( G);
3. SLSAE-answers A(zt, ... , a:n) for G -the simple equality formulas associated with success leaves of T(G).

(Base) If stratum( G) = 0, then G is an empty clause and its SLSAE-tree consists of a single node, denoted G; it is a success leaf with the associ ted SLSAE-answer true.

(Induction} Assume now that stratum( G) = m, m > 0, and that SLSAE-tree, success leaves, and SLSAE­ answers have already been defined for goals whose strata are less than m. Then

• (i) The root node ofT is G.
• (ii) If H is an arbitrary node of T labeled with <--­ Lt, ... , Ln and L = Li is the literal selected from H, then the immediate descendents of H in T( G) are de­ fined as follows:
• Suppose L is Kl, where l is not an equality literal. For each rule of the form z' <--- L~, ... , L~ such that there is an mgu e with l8 = z' e, an immediate descendent of H is labeled <--­ (Lt, ... , Li-t, L~, ... , L~, Li+t, ... , Ln)B. If there is no such rules then H is a failure node.
• If L is an equality K(tt = t2), and it and t2 are unifiable via a most general unifier e, then the im­ mediate descendent H is the goal K obtained by applying the substitution 8 to H and removing L. Otherwise (if it and t 2 are not unifiable), H has no immediate descendents and is a failure node;
• If Lis an inequality KV(tt #- t2) or -.KV(tt = t2) and if L is valid (relative to the current substitution), then the only descendent of His K = H- {L}. If L is unsatisfiable then H has no descendents and is a failure node. (Recall that R selects only valid or unsatisfiable inequalities.)
• If L is -.Kl, where l is not an equality literal. Then by definition of stratification, stratum(Kl) < m, and therefore the SLSAE-tree T( c') for c', la­ beled <--- Kl, has already been defined. By Theo­ rem 5 below, Kl f- Bt V ... V Bm is sound, 4 where {Bt, ... , Bm} is a complete-answer-set to d. By Lemma 5 and Theorem 4, there is a complete­ answer-set {A~, ... , A~} to ---, Kl. We consider three cases:
• (a) If A~ V ... VA~ = true, then the only immediate descendent of His H- {L};
• (b) If A~ V ... VA~ =false, then H has no imme­ diate descendents and is a failure node;
• (c) Otherwise, q > 0 and H has q immediate de­ scendents Hj, 1 :::; j :::; q, labeled with: 5

1. Finally, if H is labeled with an empty clause or its label contains only satisfiable, but not valid inequal­ ities, then H has no immediate descendents and is a success leaf. Its associated SLSAE-answer is a simple equality formula defined as:

where e is the substitution obtained as a composi­ tion of the previously applied most general unifiers, and 3 quantifies over all free variables not in G. 0

Theorem 5 Let P be a stratified, conservative, and solvable program. Let R be a fixed computation rule, and <--- Q be a query with a complete-answer-set {At, ... , A,.}. Then Q f-At V ... VAn is sound. 0

Theorem 6 (Soundness ofSLSAE-resolution) Let P be as above. If A is an SLSAE-answer to <--- Q, then A f- Q is sound. D

4 From now on, we write A, B, etc. instead of A.(:z:1, · · ·, :Z:n), .B(:z:1, · · ·, :Z:n)·

5 Note that equality formulas are complete, so by Lenuna 4 the appearance of K A.~ 's does not violate the syntactic form of a goal.

Theorem 7 (Completeness of SLSAE-resolution) Let P be as above,+-- Q a query toP and {A1 , ... ,.4,} a complete-answer-set to +-- Q. If A is an equality for­ mula such that A f- Q is sound, then A f- (A1 V ... VAn) is sound. 0

5 Conclusion and Future Work

We presented a fixpoint semantics for stratified and con­ servative autoepistemic programs, which uniquely deter­ mines the only iterative expansion of such a program. A resolution procedure, called SLSAE-resolution, is also defined. SLSAE-resolution is sound and complete for solvable programs. The following issues merit further investigation:

1. The results of this paper allow us to generalize the framework to permit objective clauses, not only ob­ jective literals, in the programs. Such programs are called disjunctive autoepistemic programs. Disjunc­ tive autoepistemic programs are strictly more gen­ eral than any of the current approaches in the liter­ ature that combine negation and disjunction. The following example illustrates this:

Example 2 Consider the following database:

proj1(X) V proj2(X) +-- Kstudent(X); undecided( X) +-- ·Kproj1(X), ·Kproj2(X); proj1(a); proj2(b); student(a); student(b); student(c).

The first rule says every student must be in at least one ofthe two projects proj1 and proj2. The second rule says those students who are neither in proj1 nor in proj2 have not yet decided which project to un­ dertake. Given the query +-- Kundecided(X), the answer should be X =c. Note that ·K(A VB) --+ ·K A /\ ·K B but not vise versa. Without the op­ erator K, for example in. [Ross, 1989b], this distinc­ tion can not be made, hence the first rule can be used to exclude X = c as an answer to the query +-- undecided(X). 0

1. Another issue to pursue is the efficient implemen­ tation for autoepistemic programs. For example, one may try to generalize the SYGRAF approach in [Kifer and Lozinskii, 1988] to definite and dis­ junctive autoepistemic programs.

Acknowledgements: I would like to thank Weidong Chen and Michael Kifer for many helpful discussions and invaluable suggestions. An anonymous referee's sugges­ tion is also helpful to improve the presentation of this paper.