答辩提纲.ppt

1、Assertion Answer Set Logic Program and its Application,Mingyi ZhangGuizhou Academy of Science2012-6-18,Motivation,(1) Lack of intuition Noncumulativity (Brewka,1991; Giorddano and Martelli,1994) Cause : Inconsistency between justification of defaults ( does not commit to assumptions) Example 1 Broke

2、n-arm (Pool, 1988) :Useable(x)Broken(x)/Useable(x) (1) Broken(Leftarm)Broken(Rithtarm)E=Th(Broken(Leftarm)Broken(Rithtarm), Useable(Leftarm), Useable(Leftarm),Motivation,Motivation,Adding the information x.BROKEN(x) USABLE(x) , (3)will generate two extensions as desired. This is a type of hard excep

3、tions to a default, i.e. exceptions for which the negation of the defaults consequent can be proven. In this case (1) can be replaced by :Useable(x)/Useable(x) But we hope to consider a weaker type of exception to a default: we want to block a default but we dont assert the negation of its consequen

4、t. Nonnormal defaults are needed precisely to express this weaker type of exceptions.,Motivation,Example 2 (Brewka, 1991) DOG BIRD PET DOGBIRD PET:DOG/DOG SINGS:BIRD/BIRD S1NGS . E=Th(WBIRD) which contains PET Adding PET to the DT, we get another extension which contains DOG.,Motivation,(2) Destroy

5、part of the additional expressiveness of nonnormal defaults CDL is cumulative and commits to assumptions. However, CDL is in the style of Lukaszewiczs default logic. It happens to be semimonotonic, which destroys part of the additional expressiveness of nonnormal defaults, for instance, it makes it

6、impossible to represent priorities among defaults.,Motivation,Example 3 (Giorddano and Martelli,1994) student : married/married (1) adult : married/married (2) living-in-college : student/student (3) beard : adultadult (4) living-in-college beard We want default (1) to have a higher priority than de

7、fault (2). To achieve this purpose, default (2) can be replaced with the seminormal default:adult : marriedstudent/) married (2),Motivation,The resulting theory has a single DL extension, Th(living-in-college, beard, student, adult, married), as wanted, since applying default (3) blocks (2). This sa

8、me theory, however, has two CDL extensions:F 1 containing (adult : (adult), (married : (adult, marriedstudent ) and:F 2 containing (student: student), (adult : adult), (married :student,married), since in CDL (3) blocks (2), but (2) blocks (3) in turn. Hence, in CDL, using seminormal defaults does n

9、ot allow to enforce priorities among default rules (1) and (2), as in Reiters default logic.,Motivation,To do this, Giorddano and Martelli introduced CADL (Commitment to Assumption Default Logic) and QDL(Quasi-Default Logic). Guaranteeing cumulativity of QDL, they imposed a condition on definition o

10、f QDL extension. Zhang (1999) gave the definition similar to Reiters one, algorithms for reasoning task for CADL and QDL, and a sufficient and necessary condition for cumulitiviy of QDL. (2010),Motivation,(3) Keep trace of an inference supporting a conclusion Abduction AB, B - A I. Proof in Geometry

11、 II. Diagnosis based on consistency (Reiter 1980),Motivation,A system is a pair (SD, COMPS), where SD, the system description: a set of first-order sentences COMPS, the system components: a finite set of constants. An observation of a system is a finite set of first-order sentences(SD, COMPS, OBS) -

12、 a system (SD, COMPS) with observation OBS.A diagnosis for (SD, COMPS, OBS) is a minimal set COMPS such that SD OBS AB(c) c AB(c) c COMPS is consistent.,Motivation,Proposition 1 (Zhang mingyi et al, 2004) Let (SD,Comps) be a system and OBS an observation. Given COMPS), if SDOBSAB(c) cCOPMPS- is cons

13、ist, and for any ci , is a diagnosis for any ci, SD OBS AB(c)c COMPS AB(ci), then is a diagnosis for (SD, COMPS, OBS).Proposition 2 (Reiter, 1987) - Relation between Diagnosis and premise-free normal DL Consider a system (SD, COMPONENTS) under observation OBS, where so and OBS are sets of first-orde

14、r sentences. Then E is an extension for the default theor yDT =( : AB(c)/ AB(c) c COMPS, SD OBS) iff for some diagnosis for (SD, COMPONENTS, OBS), E = predicts II.,Assertion ASP,(1) ASP- a special case of DL Assertion ASP-a special case of QDL in Reiters senseDefinition 1 An assertion is an expressi

15、on of the form , where L and S are a literal and a set of literals respectively. For any set of assertions W, we denote: Form(W)=L| , the set of literals of W. Supp(W)= , the support of W.In particular, Form(A)=L and Supp(A)=S are the literal and support of A, for an assertion A=.,Assertion ASP,Defi

16、nition 2 A rule is an expression of the form L0L1,L2, .,Lm, not Lm+1, , not Ln(m+n0), where L0, Li (1in) are literals respectively. For a set of rules R, we use the following notations:Head(R)=L0|L0L1,L2, .,Lm, not Lm+1, , not LnR(m+n0)Pos(R)= Li|L0L1,L2, .,Lm, not Lm+1, , not LnR,1im,(m+n0)Neg(R)=

17、Li|L0L1,L2, .,Lm, not Lm+1, , not LnR,m+1in,(m+n0)Write a rule as HedPos, not Neg. A rule r is basic if Neg(r)= .Definition 3 =WR is an assertion answer set program (AASP) if W is a set of assertions and R is a set of rules. =WR is basic if R is a set of basic rules. is finite iff W and R both are f

18、inite.,Assertion ASP,Definition 4 Let =WR be an AALP. A set of assertions E is an answer set of if E=0iEi , Where E0=W if Form(W) is consistent, otherwise , Ei+1=EiFi if Form( ) is consistent, otherwise .where Fi=|L0L1, L2, , LmR and Ei for 1 jm.Definition 5 Let =WR be an AASP and F a set of asserti

19、ons . The F-reduct F is an AASP obtained by removing each rR if Neg(r) Form(F) .,Assertion ASP,Definition 6 Let E is an answer set of =WR . The set of generating rules for E, GD(E,), is the set L0L1,L2, .,Lm, not Lm+1, , not LnR,(m+n0)|for i:1i m,E and for j:m+1jn,LjForm(E).Definition 7 Let =WR be a

20、n AASP. For any R,. we define an operator : (R,)=n0 n(R,), as follows: Head Pos, not Neg R Form(W)Head is consistent, 0(R,)= , otherwise HeadPos, not NegR Pos Form(W)Head(n(R,) ) and Pos Form(W)Head(n(R,) is consistent Tn+1(R,)= LLit otherwise,Assertion ASP,Definition 8 Let =WR be an AASP. RR is com

21、patible (w.r.t. ), if , for any LNeg(R), LForm(W)Head(R). R is strongly compatible if R is compatible and (R , )=R. R is -robust (or just robust, if A is understood), if R is strongly compatible and, for any R R, if R is strongly compatible, then R=R.Corollary 1 has an inconsistent answer set iff Fo

22、rm(W)Head(R*,) is inconsistent, where R*=rRNeg(r)=.Corollary 2 E= is an answer set of iff Form(W)Head(R*,) is inconsistent.Corollary 3 Suppose E is an answer set of . Then Form(E) =Form(W)Head(GR(E,) , Supp(E)=Supp(W)Neg(GR(E, ),Assertion ASP,Theorem 1. (Characterization of assertional answer sets)

23、Let =WR be an AASP. has an answer set iff there is a strongly compatible subset R of R such that, for any rRR, Pos(r) Form(W)Head(R) or (Form(W)Head() Neg(r) .Corollary 4 If R is compatible then =WR has a unique answer set.,Assertion ASP,Based on the characterization we can give an algorithm for com

24、puting answer sets and its complexity. Now we deal with the following problem, which we call the membership problem: Given an AASP , a robust set and an assertion , determine whether is an element of the answer set generated by .The main reasoning tasks in AASP are skeptical reasoning (SR) and credu

25、lous reasoning. SR: Decide whether a given assertion occurs in all assertional answer sets of . CR: Decide whether a given assertion occurs in some assertional answer set of . We derive some formal results that will allow us to deal properly with supports and to solve the membership problem.,Asserti

26、on ASP,Definition 6 Let S be a support, an AASP, and F a set of assertions. Then S = r Neg(r)S, FS = F VSLemma 1 Let be an AASP. If R is compatible, then it has a unique answer set E and GD(E, ) = (R,).Lemma 2 Let E be an answer set of a finite AASP and an assertion in E. Then the assertion is also

27、an element of E. From the definition of AASP extension, one may be tempted to think that reasoning in AASP requires exponential space, due to the combinatorial explosion of the supports in the intermediately generated assertions. However, in this paper we show that AASP has the same complexity as AS

28、P.,Assertion ASP,Theorem 2 Let be a finite AASP, a -robust set of rules, and an assertion . Let S=S. Then is an element of the answer set E of generated by iff the following two conditions (1) and (2) are satisfied:(1) LHead(S,S);(2) Neg(S,S) = S.Theorem 3 Let be a finite AASP and let be an assertio

29、n and S. (1) If Head(B) is inconsistent, then is not an element of any assertional answer set of .(2) If Head(B) is consistent, the AASP S has a unique answer set E with set of generating rules GD(E) =(S). The assertion is an element of some extension of iff E.,Assertion ASP,Lemma 3. Let be a finite

30、 AASP and an assertion such that Head(B) is consistent. Then, belongs to some answer set of iff for every , (S)S , it holds that(1) Head(), and(2) Neg() = R, where S=S.Theorem 4. In propositional AASP the reasoning tasks SR is NP-omplete, while the reasoning task CR is DP-complete.Theorem 5 AASP is

31、cumulative.,Assertion ASP,Splitting (Wu Maonian and Zhang Mingyi) Based on the Finest Splitting of Belief Set and the characterization of AASP answer sets we explored a method, which constructs a reduce without guessing a set of assertions.,Assertion ASP,Applications,(1) Alias analysis (Yang Bo and

32、Zhang Ming) Find a well tradeoff between precision and computation cost of alias analysis for some programming languages. Alias in Java program is one of the main causes for program errors. Applying AASP can determine the propagation path of points-to information more accurately, and hence improve t

33、he precision of points-to analysis.,Application,Application,ASP Rules for Points-to Analysis,ref(x,o,cs,s)pred(s,s), ref(x,o,cs,s), not ref(x,o,cs,s) (r1)reff(o,f,o,cs,s)pred(s,s), reff(o,f,o,cs,s), not reff(o,f,o,cs,s) (r2)ref(x,os,cs,s)new(s,os,x), call(m,c,cs,cs), in(s,c,m), not inbranch(s) (r3)r

34、ef(x,os,cs,s)new(s,os,x), call(m,c,cs,cs), in(s,c,m), pred(s1,s2), if(s1), branch(s2,s1), inbranch(s), same(s2,s) (r4)ref(x,o,cs,s)pred(s,s), new(s,o,x), ref(x,o,cs,s) (r5)ref(x,oy,cs,s)pred(s,s), ref(y,oy,cs,s), asn(s,x,y) (r6)ref(x,ox,cs,s) pred(s,s), ref(x,ox,cs,s), asn(s,x,y), not sp(s) (r7)reff

35、(ox,f,oy,cs,s)pred(s,s), ref(y,oy,cs,s), ref(x,ox,cs,s), store(s,x,f,y) (r8)reff(ox,f,o,cs,s)pred(s,s), ref(x,ox,cs,s), reff(ox,f,o,cs,s), store(s,x,f,y), not sp(s) (r9)ref(y,o,cs,s)pred(s,s), ref(x,ox,cs,s), reff(ox,f,o,cs,s), load(s,y,x,f) (r10)ref(y,oy,cs,s)pred(s,s), ref(y,oy,cs,s), load(s,y,x,f

36、), not sp(s) (r11),Application,sp(s) pred(s,s), ref(x,ox,cs,s), ref(y,oy,cs,s), ox=oy , asn(s,x,y) (r12)sp(s)pred(s,s), ref(x,ox,cs,s), reff(ox,f,o,cs,s), ref(y,oy,cs,s), o=oy, store(s,x,f,y) (r13)sp(s)pred(s,s), ref(y,oy,cs,s), ref(x,ox,cs,s), reff(ox,f,o,cs,s), oy=o, load(s,y,x,f) (r14)1pred(s,s):

37、branch(s,s)1if(s) (r15),Applications,Definition 9 Let P is a program and R a set of rules. R is sound w.r.t. a pointto relation of P if, for any statement StP with corresponding node s in a control flowchart such that PTSt, 1) for any reference x occurring in P, if x=ox，then ref(x,ox,cs,s) Rule(s)；

38、2) for any reference-type variable with a form x.f, if x=ox and ox.f=o，then ref(x,ox,cs,s)Rule(s) and reff(ox,f,o,cs,s)Rule(s),where PT：Stm(PSPS) is a point-to semantic relation, PS is the set of all point-to states and Stm is a set of statements formed by Assignment statement , Skip, Load, Store, S

39、equential Compound statement, Conditional statement and While statement.,Applications,Theorem 3 The set R of rules is sound w.r.t. inference of points-to relation on a program. For a diagnosis system (SD, COMPONENTS,OBS)，we call =* C the program corresponding to the diagnosis system, where *= L0L1,

40、Lm L0L1Lm CLOBS, m0R and C= L1, Lm L1LmCLOBS, m1.Definition 10 Given a diagnosis system DIS=(SD, COMPONENTS, OBS) and its corresponding standard program =* C , a diagnosis for DIS if there is an answer set S of such that,Applications,From Theorem 1 we haveTheorem 4 is a diagnosis for DIS= (SD, COMPO

41、NENTS, OBS) iff is a minimal subset of COMPONENTS such that I. ()=, where =r*H(r)COMPONENTS- and is a standard program corresponding to DIS,II. CLOBS ) is consistent.,Applications,Deal (Chen Wu, Zhang Dongmo and Zhang Mingyi)Definition 11 A bargaining game is a pair (1, 1),(2, 2), where i (i=1,2) is

42、 an AASP and i is a complete transitive and reflexive order (total preorder or weak order) over i that satisfies the following condition: for r, r1,rn i, If Pos(r) and Pos(r)Head(r1,rn) then there is k (1kn) such that rk ir.The pair (i, i i) is called the prioritized demand of player i. For any r, t

43、i, ri t denotes that r i t and ti r. rit denotes ri t and ti r. Clearly, i is an equivalent relation on i, which uniquely determines a partition of i. We use i to give a hierarchy of i, that is, each equivalent class is viewed a level of the hierarchy.,Applications,Definition 12 The sets of assertio

44、ns E1 and E2 are co-consistent if both Form(Ei)Form(E-i) and Form(Ei)SuppE-i) are consistent, where i=3-i. Definition 13 Given a prioritized demand set (,) for an agent, its hierarchy (j)j1 is defined as follows: 1=rt (rt); 1=1. for k1 k+1=rktk (rt); k+1=k k+1. It is easy to see that 1= rPos(r)=. In the sequent, we write k to denote (j)1jk.,