slides01-9.pdf

Local Strati#0Ccation #0F Instantiate rules; i.e., substitute all possible constants for variables, but reject instantiations that cause some EDB subgoal to be false. a33 Ground atom = atom with no variables. #0F Build dependency graph at the level of ground atoms by instantiating the rules. #0F Whether program + EDB is locally strati#0Ced depends not only on program, but on EDB. #0F Program + EDB is locally strati#0Ced i#0B no negative cycles in dependency graph. Example Win program with boards f1;2;3g and moves 1 ! 2, 2 ! 3, and 1 ! 3. 1 2 3 #0F The following three instantiations are the only ones that cannot be ruled out immediately by a false move subgoal: r 1 : win#281#29 :- move#281,2#29 & NOT win#282#29 r 2 : win#281#29 :- move#281,3#29 & NOT win#283#29 r 3 : win#282#29 :- move#282,3#29 & NOT win#283#29 The Dependency Graph win#281#29 win#282#29 win#283#29 move#281,3#29move#281,2#29 move#282,3#29 ,, , #0F The three move ground atoms and win#283#29 are in stratum 0; win#282#29 is in stratum 1, and win#281#29 is in stratum 2. 1 Computing the Locally Strati#0CedModel Compute locally strati#0Ced #28#5Cperfect"#29 model bottom-up, deciding on the truth or falsehood of atoms by computing the LFP of each stratum in turn. Example Stratum 0: We #0Cnd win#283#29 is false. Stratum 1: That lets us use r 3 to infer win#282#29 is true. Stratum2: We then use r 2 to infer win#281#29 is true. Stable Models Intuitively, model M is #5Cstable" if when you apply the rules to M you get exactly M back. Example #5CWin" rule: win#28X#29 :- move#28X,Y#29 & NOT win#28Y#29 with EDB 1 ! 2, 2 ! 3, 1 ! 3. 1 2 3 #0F M = EDB + fwin#281#29;win#282#29g is stable. #0F The three useful instantiations are r 1 : win#281#29 :- move#281,2#29 & NOT win#282#29 r 2 : win#281#29 :- move#281,3#29 & NOT win#283#29 r 3 : win#282#29 :- move#282,3#29 & NOT win#283#29 #0F M makes only the bodies of r 2 and r 3 true, letting us infer exactly M. #0F Note you get the EDB facts #5Cfor free" in this process. Gelfond-Lifschitz Transform Formal notion of applying rules to a model M. 1. Instantiate rules in all possible ways. 2. Delete instantiated rules with a #28nonnegated#29 EDB subgoal that is not in M or with a false arithmetic subgoal. a33 Remember, EDB is part of M. 2 3. Delete instantiated rules with a subgoal NOT p#28x#29, where p#28x#29isinM. a33 In #283#29 and #284#29, p can be either EDB or IDB. 4. Delete any subgoal NOT p#28x#29 if p#28x#29 is not in M. 5. Delete any EDB subgoal in M and any true arithmetic subgoal. #0F What's left? Rules with zero or more nonnegated, relational subgoals with IDB predicates. a33 Note that a rule with emptybodyisan assertion that the head is true. #0F GL#28M#29 = EDB + result of inferring IDB with the remaining rules. Bottom Line on GL Transform You can use negative EDB or IDB facts in M #28i.e., atoms missing from M#29 to help infer facts, and you use positive EDB facts, but you don't use the positive IDB facts in M unless you derive them from other facts. Formal De#0Cnition of Stable Models #0F If GL#28M#29=M, then M is stable. #0F The #5Cstable semantics" for a program + EDB is the unique stable model with that EDB, if there is one. a33 Sometimes it is interesting to look at the set of stable models, as well. Example M = fmove#281;2#29, move#281;3#29, move#282;3#29, win#281#29, win#282#29g #28formal version of previous example#29. #0F After step #282#29: r 1 : win#281#29 :- move#281,2#29 & NOT win#282#29 r 2 : win#281#29 :- move#281,3#29 & NOT win#283#29 r 3 : win#282#29 :- move#282,3#29 & NOT win#283#29 #0F After step #283#29: r 2 : win#281#29 :- move#281,3#29 & NOT win#283#29 r 3 : win#282#29 :- move#282,3#29 & NOT win#283#29 #0F After step #284#29: 3 r 2 : win#281#29 :- move#281,3#29 r 3 : win#282#29 :- move#282,3#29 #0F After step #285#29: r 2 : win#281#29 :- r 3 : win#282#29 :- #0F Thus, GL#28M#29=fwin#281#29;win#282#29g + EDB = M. #0F M is a stable model. Example Consider the #5Cprogram": p#28X#29 :- p#28X#29 #0F ; is the only stable model. #0F Why? The only instantiated rules are of the form p#28a#29 :- p#28a#29. a33 The GL transform doesn't a#0Bect these, no matter what M is. a33 Thus, there is no way to infer any p#28a#29. Example For any Datalog program without negation, the unique LFP is the only stable model. #0F Why? To test whether M is stable, we compute GL#28M#29. a33 Since there is no negation in bodies, the surviving instantiated rules are exactly the ones with true EDB subgoals. a33 Thus, GL infers exactly the LFP for the EDB portion of M, regardless of what M is. a33 If we start with the LFP,we infer it, so that model is stable; if we start with another model, we still infer the LFP,so that model is not stable. PropositionalStable Models It is often useful to #0Cnd propositional examples. #0F No EDB in propositional logic. #0F Thus, only steps #283#29 and #284#29, plus the #0Cnal inference, are relevant for the GL transform. 4 Example p :- q; q :- NOT r; r :- s; s :- NOT p #0F M = fp;qg. #0F After step #283#29: p :- q; q :- NOT r; r :- s #0F After step #284#29: p :- q; q :- ; r :- s #0F Inference: GL#28M#29=fp;qg = M. MultipleStable Models Possible Notice that fr;sg is also a stable model of the above rules. 5 small9.dvi