Derivation Procedures for Extended Stable Models

1 Introduction

Well Founded Semantics (WFS) [Van Gelder et al., 1990] adequately captures various forms of hypotheti­ cal reasoning [Pereira et al., 1991c, Pereira et al., 1991d, Pereira et al., 1991b, Pereira et al., 1991a] if we inter­ pret the well-founded model (W F M) of a program II as a (possibly incomplete} core view of the world, the extended stable modds (XSMs) specifying alternative complementary consistent views of the world, all of each containing the core W F M.

The paper is organized as follows: in section 2 we review well founded semantics. In section 3 we de­ fine W F M-derivations, discuss their correctness, and give examples. Next, in section 4, we define XSM­ derivations and discuss their correctness. Finally, in sec­ tion 5, a Prolog implementation is produced, directly reflecting the derivation procedures mentioned. More details can be found in an extended version of this paper [Pereira et al., 1990].

By a logic program II we mean a finite set of univer­ sally closed rules of the form: H - L1 , ... , Ln where n ~ 0, H is an atom and the L;'s are literals. When n = 0, we also write H - t, where t stands for an atom satisfied in all models. Negative literals are expressed as .-vA where A is an atom. We denote by Lit{II) the set of literals in ground{II), the Herbrand instantiation of program II. We denote the well founded model of a program II by W F M(IT), and an extended stable model (which may be the well founded one) by XSM(IT).

2 The Extended Stable Model Semantics

In this section we characterize the Well Founded and Extended Stable Models of a program, based on [Przy­ musinska and Przymusinski, 1990]. Alternative defini­ tions of the Well Founded Semantics can be found in [Van Gelder et al., 1990] or in [Przymusinski, 1989]. Be­ cause the semantics is 3-valued, we begin by defining 3-valued interpretations.

Definition 2.1 A 3-valued Herbrand interpretation I of a first-order language Lis any pair (T; F), where T and F are disjoint subsets of the Herbrand base H. T con­ tains all ground atoms true in I, F contains all ground atoms false in I, and the truth value of the remaining atoms, those in U = H - (T U F), is undefined (or un­ known).

An alternative way to represent an interpretation I = (T; F) is I= T U { .-vLjL E F}.

Proposition 2.1 Any interpretation I= (T; F) can be equivalently viewed as a function I : H -+ V where V = {0,1/2,1}, defined by:

• I (A) = 0 if A E F
• I(A) = 1/2 if A E U
• I (A) = 1 if A E T

Definition 2.2 The function I : H -+ V can be re­ cursively extended to the truth valuation function i : Lit(IT) -+ V defined on the set Lit(II) of all literals of the language as follows, where A is a ground atom:

• i(A) = I(A)
• z(.-vA) = 1- I(A)

Definition 2.3 A non-negative program is a program whose premises are either positive atoms or the special proposition u. Every interpretation I satisfies I(u) = 1/2, and so i(.-vu) = 1/2. u denotes the undefined (or unknown) value.

Theorem 2.1 (Generalization of [Van Emden and Kowalski, 1976]} Every non negative logic-program has a unique least 1 3-valued model.

1 If I and J are two intgerpretations then we say that I ~ J if I(A) ~ J(A) for any ground atom A. If I is a

Next we define the program transformation II/M (II modulo M), which is a 3-valued extension to the 2-valued transformation in [Gelfond and Lifschitz, 1988].

Definition 2.4 Let II be a logic program and let I be a 3-valued interpretation. By the extended G £­ transformation of II modulo I we mean a new (non­ negative) program II/ I obtained from II by performing the following three operations:

• Removing from II all rules which contain a negative premise L ="'A such that i(L) = 0.
• Replacing in all remaining rules those negative premises L ="'A which satisfy i(L) = 1/2 by u.
• Removing from all the remaining rules those nega­ tive L ="'A which satisfy i(L) = 1.

Since the resulting program II/ I is non-negative, by theorem 2.5, it has a unique least 3 valued model. We define f*(I) (a generalization of the r operator [Gelfond and Lifschitz, 1988]) to be the 3-valued least model of IIJI.

Definition 2.5 A 3-valued interpretation I of a logic program II is called an Extended Stable Model XSM of II iff f*(I) =I.

In order to check if I is an XSMof a program we give a constructive definition of f* operator. For this pur­ pose we define '11*, a generalization of the Van Emden­ Kowalski operator '11.

Definition 2.6 Let II be a non-negative program, I an interpretation of II and A is a ground atom. Then 'l!*(I) is an interpretation defined as follows:

• 'l!*(I)(A) = 1 iff there is a rule A+- AI.··· ,An in II such that I(A;) = 1 for all i ~ n.
• 'l!*(I)(A) = 0 iff for every rule A+- A1, ... ,An in II there is an i ~ n such that I(A;) = 0.
• '11 * (I)(A) = 1/2, otherwise

Definition 2. 7 Let I be an interpretation and II a logic program. f*(I) for II can be defined as f*(I) = l!i*Tw(IIji).

This alternative definition of the W F semantics was proved eq.uivalent to the original one [Van Gelder et al., 1990] in [Przymusinska and Przymusinski, 1990] by the following theorem:

Theorem 2.2 The Well Founded Model of a program IT is the F-least 2 Extended Stable Model of IT. Conse­ quently the WFS coincides with the XSMS.

collection of interpretations, then an interpretation I E I is called minimal in I if there is no interpretation J E I such that J $ I and I =/= J. An interpretation I is called least in I if I ~ J, for any other interpretation J E I. A model of a theory R is called minimal (resp. least) if it is minimal (resp. least) among all models of R.

2 If I = (T, F) and I' = (T', F') are two interpretations, then we say that I ~F I' iff T ~ T' and F ~ F'. An inter­ pretation I is called F-least in a collection of interpretations I if I $F J for any interpretation J E I [Fitting, 1985)

To obtain a constructive definition of the W F M of a program II we use the following sequence of {I<>} of interpretations of II:

• Io = {{}, {}}
• Ia-+1 = f*(Ia-)

The W F model of IT is the least fixed point of this se­ quence, i.e. I>. [Przymusinska and Przymusinski, 1990].

3 Derivation Procedure for the Well Founded Model

Now we present a derivation procedure such that given a program II and a goal G the derivation succeeds iff G is in W F M(IT). The procedure is defined over the ground instance of IT, the set of all ground instances of the rules in IT with respect to its Herbrand Universe. Without loss of generality we can assume that IT has been already instantiated and thus consists of a (possibly infinite) set of propositional rules.

Definition 3.1 A positive (resp. negative) interpreta­ tion I is a set of positive ( resp. negative) literals from Lit(IT).

Definition 3.2 A context. Cn is an ordered set of pos­ itive or negative interpretations. Let S; be a positive or a negative interpretation; Cn denotes the context S1S2 ··· Sn. Cn is a negative (resp. positive) context if Sn is a negative interpretation (resp. positive interpreta­ tion). Cn + G denotes the concatenation S1S2 ··· SnG. A literal G is in context Cn ( G E Cn for short) G E Sn.

A context C,. implicitly defines an interpretation In(Cn) which is the set of literals in partial interpretations S,. i.e. I,.(Cn) = U(i~n)Si, and for no atom A both A and "'A belong to it.

Definition 3.3 A contextual formula (C-formula) is a pair C#F, where C is a context and F is an expression built from atoms with conjunctions and negations. An empty C-formula is the C-formula C#t.

By the interpretation I( C#F) we mean the interpre­ tation I(C) associated with context C.

Definition 3.4 {WFM-derivation) Let

Rj = {Cj#Fi; Ij} where Cj is a context, and Ij a set of literals. A W F M -derivation from R; to Rn is a se­ quence from< C;#F;; I; > to < Cn#Fn; In > such that forany (Ck#Fk;h} (i ~ k ~ n), the following derivation rules apply (where we assume Ck+l = Ck and Ik+l = h unless stated otherwise).

Dl.l. if Fk ="' G and there is no rule G +- B then RH1 = {Ck+ "'G#t;h U {"'G}}.

D1.2. if Fk ="'G and ~ E Ck then FH1 = t.

D2.1. if Fk ="'G and there are r rules for G with G; (1 ~ i ~ r) as head, "'G ¢ Ck, G ¢ Ik

in IT and G ~ Ik, then"' Rk+I = (Ck+ "'G# G1, ... , Gr; Ik U { "'G}} where G; is a short hand for "-'(Eli, ... , Bm;)

• D2.2. if Pk ='""' (G1. ... , Gm) then Rk+1 = (Ck# ,...., G;; h) for some 1 :5 i :5 m.
• D3. if Pk = G and G ~ h then for some rule G +-- Bl,··· ,Bm E II, Rk+l = (Ck + G#(BI.··· ,Bm);Ik U {G})
• D4. if Pk = (g, G) then Rk+l = (Ck#G; I 9 k) if there is a derivation from (Ck#g;Ik) to (L#t;Igk}·

There is a WPM-derivation for G in II iff there is a sequence from ( {}#G; {}) to (L#t; I}, for some I.

We argue these rules are intuitive when one recalls the definition of 3-valued model [cf. section 2]: rule Dl.1 establishes the CW A 3 · Rule Dl.2 says that a literal may support on itself when proving its falsity 4 · Rule D2.1 says that for an atom to be interpreted as false it has to be proven false in all definitions for it. Rule D2.2 says that for a body of a rule to be false it is enough to prove some literal in the body to be false 5 · Rule D3 says that for a literal to be true it is enough to have a rule with all body literals true 6 · Rule D4 says that a conjunction of formulas is true if each element is true. Note that Ik = Ui<n I;U{Pk} if Pk is a literal. This means we don't need to explicitly record Ik at each step k but simply consider all the Cj in (j < k). Note that rule D4 introduces a notion of sub-derivation. We now present examples illustrating the application of the derivation rules.

Example 1 For the program II= {p +-,....,q}, a WPM­ derivation for p is:

Example 2 Let II be the "work-tired" example [Przy­ musinski, 1990] with the obvious abbreviations:

A failed derivation for ,...,a is:

3 Note that according to the second point of the definition of the w· operator, if an atom A has no rules in II, then w·(I)(A) = 0 for all interpretations I of P.

4 According to the definition of w·fw' we start with w·fO = ({},H). So every negative literal may depend on itself. There is no corresponding rule for positive literals

5 Again these two rules follow exactly the second point of definition 2.6

6 This is what is stated in the first point of the definition of w·

and a successful derivation for ,...,a:

Example 3 There is no derivation for (p, q) in program II = {p +-,....,q, q +-"'P }.

Note that even the selected literal order differed the derivation definition is still applicable because we keep a record of Ik at each derivation step.

3.1 WPM-Trees

A derivation from (0#G; 0} to (L#t; I} may be inter­ preted as the construction of certain trees to be intro­ duced now. These trees are obtained from the derivation rules with the following in mind: at each derivation step (Ck#Lk; h), Ck is the ordered ancestor list of literal Lk which is a node of the tree, and h is the set of all literals in the nodes already visited by the derivation procedure. In the following we will omit the special symbol t.

Definition 3.5 (WPM-Tree) A WPM-tree for G given program II WPM( G, II) is a finite tree with root G, such that if N is the literal of a node of the tree then:

WFM-1 If N is negative, let N =,....,£ and:

1. if there are no rules for L then N is a leaf (rule D1.1)
2. if,....,£ has an identical ancestor A and all literals in the branch from ,....,£ to A are negative then N is a leaf (rule D1.2)
3. if there are r rules for L: (rules D2.1+D2.2)

in II, then node ,...., L has r immediate descen­ dents ""Bji,····""Bhn each one selected from the body of a different rule.

WFM-11 If N is positive then:

1. If there is a fact N in II, then N is a leaf (rule D3)
2. the n immediate descendents are those literals B1 ... Bn, such that a rule N +-- B1 , ... B 71 ex­ ists in II (rule D4)

By considering all possible choices of rules and literals all WFM-trees are obtained.

Proposition 3.1 For every program II and goal G there is a WPM -derivation for G in II iff there is a W F .M­ Tree(G,II).

Note that a context C in a C-formula C#L, expresses a branch from the root of the tree to node L. Given a tree and a node, its context is implicitly defined by the ordered set of its ancestors, with its father being the most recent one in C (the rightmost). The condition G ~ Ik in D2.1 and D3 means that if a tree has a node L (resp. "'L) then it may have no node "'L (resp. L).

We may think of the derivation rules as stating con­ ditions for re-writing a literal, possibly by cancelation with a previous ancestor in the tree. For the well founded model derivation procedure the only possible cancelation of a literal with an ancestor is provided by rule D1.2.

Example 4 The WFM-Tree for p given program {p +-"-'q} is:

Example 5 The W F M-Tree for "'a for the program below is:

Example 6 The W F M-Tree for "'a for the program below is:

Note theW F M of this program is {"'a, "'T, "-'q}.

3.2 Properties of WPM-Trees

By definition W F M-Trees are finite. The only type of leaf nodes in a W F M-tree are:

1. a positive literal with no identical ancestor
2. a negative literal with no identical ancestor
3. a negative literal with an identical ancestor

Proposition 3.2 Every branch from the root literal has at most one node with an identical ancestor.

Proposition 3.3 If a leaf node for literal L has an iden­ tical ancestor then L is a negative literal.

Proposition 3.4 If a leaf node for literal L has no iden­ tical ancestor and is a negative literal L ="'H then there are no rules for H in 11.

Proposition 3.5 If a leaf node has a positive literal L then no node in the branch from the root literal to L has an identical ancestor literal, and there is a fact L in program 11.

Lemma 3.1 (Leaves are in the W F M) If T is a WFM(G,II) tree for Gin 11 then:

1. a positive literal which is in a leaf node, and has no identical ancestor, is in W F M(II)
2. a negative literal which is in a leaf node, and has no identical ancestor, is in W F M(II)
3. a negative literal which is in a leaf node, and has an identical ancestor is in W F M (11)

Proof:

• 3.1.1) if a positive literal L is in a leaf node, and has no identical ancestor, then there is a fact L in 11 and facts are always in W F M(II).
• 3.1.2) if a negative literal "'L is in a leaf node, and has no identical ancestor, then there are no rules for L in 11. For an atom L such that no rules for it exist in 11, "'L is in W F M(II).
• 3.1.3) if a negative literal "'L is in a leaf node and has an identical ancestor, we have:

i.e. there is at least one chain from L to L, and possibly a rule for L, such as (3) in the program below:

1. L+- ... H .. .
2. H +- ... L .. .
3. L +- Bt ... Bn

i.e. in 11 there is a chain of positive literals L ... H ... L, and the well founded model contains "'L ... "'H ... "'L.

Note that for the model not to contain "'L by (3) all B; would have to differ from false. But in that case the tree named B; in the figure above could not exist, nor the father node "'L.

Lemma 3.2 Given a W F M-tree for G then, for any internal node literal H, if its immediate descendents D1 ··. Dn are in the well founded model, then H is in the WFM.

Proof:The prooffollows easily from the observation that the only tree formation rules introducing descendents nodes are WFM-1.3 and WFM-11.2 and the definition of 3-valued interpretation ( cf. footnotes 5 and 6).

Theorem 3.3 (Soundness ofWFM-Trees) Let 11 be a program and L a literal. If there is a W F M-tree for L then Lis in W F M(II).

Proof: Follows directly from lemma 3.1 and lemma 3.2 above.

Corollary 1 Given program 11 and literal G such that G E W F M(II) then all literals in the W F M( G, II) arc in WFM(II).

Theorem 3.4 (Completeness of W F M trees) Let 11 be a program and L a literal. If L is in W F M(IT) there is a W F M-tree for L.

Proof: Appears in the extended version.

4 Derivation Procedure for Extended Stable Models

We present now a derivation procedure such that, given a program IT and a literal G, the derivation succeeds if G is in some XSM(IT).

Definition 4.1 {X SM -Derivation)

Let R; = (C;#F;;I;) where C; is a context and I;a set of literals. A XSM-derivation from R; to Rn is a sequence from (C;#F;; I;) to (Cn#Fn; In) such that for any (Ck#Fk;Ik) (i ~ k ~ n) the following derivation rules apply (where we assume Ck+l = Ck and Ik+l = Ik unless stated otherwise):

D1.1 if Fk ="' G and there is no rule G - E then Rk+l = (Ck+ .-vG#t;Ik U {.-vG})

D1.2 if Fk ="'G and "'G E Cm, m ~ k then Fk+l = t D2.1 if Fk =.-vG, .-vG ¢ ck, G ¢ Ik, and there are T rules for G with G; as head

"' "' m IT then CH1 = Ck+ "' G# G1, ... , Gr, and Ik+1 = IkU "'G where G; is a short hand for .-v{EI;, ... , Em;)

• D2.2 if Fk ="'( G1, ... , Gm) then

Rk+l = (Ck# .-vG;; Ik) for some 1 ~ i ~ m

• D3.1 if Fk = G, "' G ¢ Ik and G ¢ Ik then for some rule G - E1, ... ,Em in IT, Rk+l = (Ck + G#(EJ. ... ,Em);Ik U {G})

D3.2 if Fk = G and G E Cm (m < k) then Fk+I = t

D4 if Fk = (g, G) then Rk+l = (Ck#G; I 9 k} if there is a derivation from (Ck#g; Ik) to (L#t; Igk}·

Note these derivation rules include, as expected, those for well WFM-derivations.

Example 7

A XSM-derivation for a is as follows:

The X S M -derivation for .-va is as follows:

4.1 XSM-trees

Definition 4.2 {XSM-tree) A XSM-tree for G given program IT, XSM(G,IT) is a finite tree with root G, such that if N is the literal of a node of the tree then:

XSM-1 If N is negative, then N = .-vL and:

1. if there are no rules for L then N is a leaf (rule D1.1)
2. if .-vL has an identical ancestor A and all literals in the branch .-vL to A are negative then N is a leaf (rule DL2)
3. if there are r rules for L: (rules D2.1+D2.2)

in IT, then node "'L has r immediate descen­ dents "'E;1 ··· "'Ehn each one selected from the body of a different rule

1. if "'L has an identical ancestor A with some positive literal in between, then N is a leaf (rule D1.2)

XSM-11 If N is positive then:

1. if there is a fact N in II, then N is a leaf (rule D3.1)
2. the n immediate descendents are those literals E1 ... En, such that a rule N +- B1 .. . B" ex­ ists in II(rule D4)
3. if N has an identical ancestor A, with some negative literal in between, then N is a leaf (rule D3.2)

A XSM-Tree has two types of leaves not appearing in the W F M -Tree, namely: i) positive literal leaf nodes having an identical ancestor and with some negative lit­ eral in between; and ii) negative literal leaf nodes having an identical ancestor and with some positive literal in between.

Example 8 Although the program {a ,_,..., b; b +-'"'-'a} has no WFM-Tree it has the following XSM-Trees (among others):

The soundness proof is similar to that of vV F M-Trees, but the equivalent to lemma 3.1 is now:

Lemma 4.1 (Leaves are in the XSM}If Tis a XSM tree for G then:

• 4.1.1) a positive literal in a leaf node, having no iden­ tical ancestor, is in some XSM(IT)
• 4.1.2) a negative literal in a leaf node, having no identical ancestor, is in some X S M (IT)
• 4.1.3) a negative literal in a leaf node, having an identical ancestor, is in some XSM(IT)
• 4.1.4) a positive literal in a leaf node, having an iden­ tical ancestor and some negative literal in between, is in some XSM(IT)
• 4.1.5) a negative literal in a leaf node, having an identical ancestor and some positive literal in be­ tween, is in some XSM(IT)

Proof: Proof of 1,2 and 3 4.1.i, 4.1.ii and 4.l.iii fol­ lows from lemma 3.1 and the fact that all literals in the WFM(IT) are in all XSM(IT).

4.2 Completeness of XSM-Tree

The completeness proof may be found in the full version.

5 A Prolog implementation

'vVe present here a Prolog implementation of the above procedures which provides them with an operational se­ mantics. Lines are numbered for referencing. The inter­ preter is basically the implementation of the derivation rules of the procedures [cf. section 3 and 4] plus loop checking. Thus the execution always terminates. The code may be used for W F M-derivations as below, or for X 3M-derivations by deleting line (7.4).mb is the member predicate.

s("' ((G1,G)) ,I,O,An) :- s(-G1,I,O ,An). (1) s("' ((G1,G)) ,I,O,An) :-! ,s("' (G) ,I,O ,An). (2) s((G1,G),I,O,An):-!,s(G1,I,II,An),s(G,II,O,An). (3) s("' (-G) ,A ,B ,C ) :- ! , s(G,A,B,C). (4) s("'G,I,_,An) :- mb(G ,I),!, fail. (5) s( G,I,_,An) :- G "'(_), mb("'G,I), ! , fail. (6) s(G,I, [G!I] ,An) :- d(G,An,D), (7) ( D · z, G · (,...,_), !; D · z, !, fail; D = e, !, fail; % wfm (7.4) D = e, ! ) . s("'G,_ ,_ ,_ ) :- (G «- ) , ! , fail. (8) s("-'G,I,O,An) :- ! , findall((G«-B), (G«-B) ,L), (9) alLou t ("' G , L , ["' G I I] , 0 , ["' G I An]) . s(G,I, [G!I] ,An) :- (G «- ) . (10) s(G,I,O ,An) :- (G«-B) ,s(B, [G!I] ,0, [G!An]). (11) alLout("' G, [] ,I,I,An) . (12) alLout("' G, [(G«-(B1)) !Gn] ,I,O,An) :- (13) s ("' (B1), I, II ,An), alLout ("' G ,Gn, II, 0 ,An). d("'G, [("'X) !An] ,D) :- ! , d("'G, [("'X) !An] ,e,ZNZ,D). d("'G, [ X !An] ,D):-! ,d("' G, [ X !An] ,o,ZNZ,D). d(G, [("-'X) !An] ,D):-! ,d( G, [("'X) !An] ,o,ZNZ,D). d(G,[ X!An] ,D):- d( G,[ X !An],e,ZNZ,D). d(G,[G!T] ,e ,Z ,z) :- var(Z), !. d(G, [G!T] ,D ,nz,D) :- ! . d ( G , [ ("' _) , ("' X) I T] , EO , Z , D) : - ! , d ( G , [ ("' X) I T] , EO , Z , D) . d(G, [("'_),(X) IT],e,_,D) : -! ,d(G, [X IT] ,o,nz,D). d(G,[("-'_),(X) IT],o,_,D) :-!,d(G,[XIT] ,e,nz,D). d(G,[_ ,("'X)!T],e,_,D) :-!,d(G,[(,...,X)IT],o,nz,D). d(G, [_ , (-X) IT] ,o,_,D) :-! ,d(G, [("'X) IT] ,e,nz,D). d(G, [_ ,X IT] ,EO,Z ,D) :- d(G, [X IT] ,OE,Z,D). (25)

Lines (1)-(2) correspond to rule D2.2. Line (3) cor­ responds to rule D4. Line (4) is obvious. Lines (5)-(6) ensure the condition G ¢ h. Lines (9), (12) and (13) correspond to D2.1. Lines (14) - (25) do an ancestor search for literal G: the result of this search can be: the literal G has an ancestor node in the current context (D=z) ;the literal G has an ancestor node in some context other than the current one; the literal G has no ances­ tor goal and the predicate dist/3 in rule (7) fails. Line (7.2) corresponds to derivation rule D1.2. Line (7.5) cor­ responds to rules D1.2 and D3.2. Line (12) accounts for rule Dl.l. Line (7.3) avoids the potential loop of a posi­ tive literal G with an identical ancestor G with no nega­ tive literals in between. A literal G is in W F M(IT) (resp. XSM(ll))ifthequery?- s(G,[].L,[]) succeeds. The procedure returns in La set of literals in theW F M(IT) (rcsp. XSM(IT)).

Acknowledgements

We thank ESPRIT BRA COMPULOG (no. 3012) , INIC, JNICT and Gabinete de Filosofia do Conheci­ mento.