Defaults Involving Functions Date: 17 Apr 2012 From: Vladimir Lifschitz To: TAG I am reading now the KR'12 paper by Mike Bartholomew and Joohyung Lee (http://peace.eas.asu.edu/joolee/papers/fsm-kr.pdf), and I found there an interesting observation that the authors have unfortunately hidden in the middle of a highly technical discussion, where it can be easily overlooked. How does ASP solve the frame problem, say, in the blocks world? The traditional way of doing that is to write % inertia on(B,L,T+1) :- on(B,L,T), not -on(B,L,T+1), T This alternative formulation is more economical, because it eliminates > the need for strong negation. I am not sure why it is more economical. The first (old) solution "eliminates" need for choice rules and cardinality constraints. ============== Date: 19 Apr 2012 From: Joohyung Lee To: TAG To me a more economical way is to write as {loc(B,T+1)=L} :- loc(B,T)=L, T Paolo correctly states that the new solution only works if > each block is assumed to be supported by table or other block. > I normally do not make this a necessary part of the blocks world > story. I normally make this assumption when dealing with multi-valued fluents in answer set planning. In each state, every block has a location (other block or the table). I wonder when we need to avoid this assumption. Could you please tell me? --- Note that the blocks world was chosen intentionally in that paper to avoid the use of strong negation. There is one place where strong negation is a bit more economical even with the new encoding, when we express Boolean fluents. Consider {up(true,T+1)} :- up(true,T), T (I hope someday an answer set solver (or its preprocessor) > can directly accept a rule like (1) ). I don't know if it's what you are looking for, but in the past several months I have been working on a solver that among other things accepts directly the syntax of (1) -- modulo small syntactic variations. The solver is called clingof, is based on clingo and is available from http://marcy.cjb.net/clingof/. The last example on the web page shows the use of choice rules similar to (1). In the language of clingof, (1) would be written: { loc(B,T2) #= L } :- loc(B,T1)#=L, time(T1), block(B), loc(L), T1 and add the existence constraint > > :- {up(T), -up(T)} 0. Constraints like these always make my brain heart, since in a way they carry more negation, intuitively. Why not write up(T) v -up(T). ============== Date: 7 May 2012 From: Vladimir Lifschitz To: Gerald Pfeifer It seems to me that your formulation is much too strong, it would make the usual ASP solution to the frame problem invalid. The program up(0). up(1) :- up(0), not -up(1). has one answer set: {up(0), up(1)}. But adding the rule up(1) v -up(1). will add one more answer set, {up(0), -up(1)}, in conflict with the idea of inertia. I agree that the rule :- {up(T), -up(T)} 0. (or, in the dlv syntax, :- not up(T), not -up(T).) is "negative", but this is exactly what we want. It expresses the "negative" idea that incomplete answer sets do not represent states and consequently should be dropped.